No description, website, or topics provided.
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
src
.project
License.txt
ReadMe
configure
configure_tmp.sh
runExperiment

ReadMe

naum abstracts a given set of formulas into a 
conjunction of formulas that has a certain structure.
The structure could be the functions in the abstracted 
formulas and/or number of conjunctions in the learnt 
abstraction. 

Dependencies:

*Python packages:
--oct2py
--cvxopt
--cvxpy
--numpy

*Proteus

Inputs to naum:
*Basis functions for the classifier
*The set of formulas to be abstracted in 'dr' format (see dReal library of 
benchmarks for help) 
*Other learning parameters -- number of conjunctions in each classifier
*Number of formulas to be abstracted together
*Decomposition mode -- Hamming based/Bound based/etc...

Output: 
The output from 'naum' is an abstracted 
representation of a given set of constraints 
that is simpler for an SMT solver to handle.

Usage:
1. Clone the repo to a local drive

2. Navigate to naum/ and run 
$./configure
$./configure_tmp.sh

2.Create a file with constraints in the 'dr' format

3. To abstract and solve your set of constraints from 
inside naum:
$cd bin
$Naum <dr file name> <parameters>
where <parameters> -- sequence of five 0/1-s
First position in parameter indicates whether to check for sat
Second position is parameter indicates whether to check for unsat
Third position is for Hamming Based Decompositon
Fourth Position/Fifth are inactive currently -- so set to 0