diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-01 11:18:00 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-01 11:18:06 -0600 |
commit | 0615601703a1ac19d485e2b530a748c797b544ed (patch) | |
tree | 19834cce797501d5586aed222349933c9af16b4a /src/theory/quantifiers | |
parent | 2ba8bb701ce289ba60afec01b653b0930cc59298 (diff) |
Simplify fmc model construction, add regression. Improve FMF debug assertions.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 29 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 3 |
3 files changed, 30 insertions, 5 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 018a0c3e0..aa2a43fbf 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -669,6 +669,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) { Node v = d_models[op]->d_value[i]; Trace("fmc-model-func") << "Value is : " << v << std::endl; + Assert( v.isConst() ); + /* if( !hasTerm( v ) ){ //can happen when the model basis term does not exist in ground assignment TypeNode tn = v.getType(); @@ -685,6 +687,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { } } v = getRepresentative( v ); + */ if( curr.isNull() ){ Trace("fmc-model-func") << "base : " << v << std::endl; curr = v; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 56f966426..6dfd4c737 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1605,10 +1605,10 @@ bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) { } bool TermDb::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ) { - if( std::find( t.begin(), t.end(), n )!=t.end() ){ - return true; - }else{ - if( visited.find( n )==visited.end() ){ + if( visited.find( n )==visited.end() ){ + if( std::find( t.begin(), t.end(), n )!=t.end() ){ + return true; + }else{ visited[n] = true; for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( containsTerms2( n[i], t, visited ) ){ @@ -1616,8 +1616,22 @@ bool TermDb::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, boo } } } - return false; } + return false; +} + +bool TermDb::containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited ) { + if( n.getKind()==UNINTERPRETED_CONSTANT ){ + return true; + }else if( visited.find( n )==visited.end() ){ + visited[n] = true; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( containsUninterpretedConstant2( n[i], visited ) ){ + return true; + } + } + } + return false; } bool TermDb::containsTerm( Node n, Node t ) { @@ -1634,6 +1648,11 @@ bool TermDb::containsTerms( Node n, std::vector< Node >& t ) { } } +bool TermDb::containsUninterpretedConstant( Node n ) { + std::map< Node, bool > visited; + return containsUninterpretedConstant2( n, visited ); +} + Node TermDb::simpleNegate( Node n ){ if( n.getKind()==OR || n.getKind()==AND ){ std::vector< Node > children; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 86b0efbf3..0c4e94517 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -397,12 +397,15 @@ private: //helper for contains term static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited ); static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ); + static bool containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited ); //general utilities public: /** simple check for whether n contains t as subterm */ static bool containsTerm( Node n, Node t ); /** simple check for contains term, true if contains at least one term in t */ static bool containsTerms( Node n, std::vector< Node >& t ); + /** contains uninterpreted constant */ + static bool containsUninterpretedConstant( Node n ); /** simple negate */ static Node simpleNegate( Node n ); /** is assoc */ |