diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-09 09:51:52 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-09 09:51:52 -0600 |
commit | 22b211647501a4dad5cec66c2ea6383ea8e7b7bd (patch) | |
tree | c4d3f95a8706dfd3c74d73e2d875bda09ef0fd90 /src | |
parent | a9cf481470c324a04f2254c5745eee26c45cb309 (diff) |
Decouple sygus term database and term database. (#1317)
* Decouple sygus term database and term database.
* Clang format
* Fix include
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database_sygus.cpp | 42 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database_sygus.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 19 |
4 files changed, 44 insertions, 35 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a3225e404..5db58067f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -14,20 +14,12 @@ #include "theory/quantifiers/term_database.h" -#include "expr/datatype.h" #include "options/base_options.h" #include "options/quantifiers_options.h" -#include "options/datatypes_options.h" #include "options/uf_options.h" -#include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/fun_def_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/rewrite_engine.h" -#include "theory/quantifiers/theory_quantifiers.h" -#include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers/trigger.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" @@ -250,10 +242,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi d_ops.push_back(op); d_op_map[op].push_back( n ); added.insert( n ); - - if( d_quantEngine->getTermDatabaseSygus() ){ - d_quantEngine->getTermDatabaseSygus()->registerEvalTerm( n ); - } } }else{ setTermInactive( n ); diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index f298e9711..d8d120eab 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -1912,32 +1912,38 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) { void TermDbSygus::registerEvalTerm( Node n ) { if( options::sygusDirectEval() ){ if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){ - Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n - << std::endl; TypeNode tn = n[0].getType(); if( tn.isDatatype() ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); if( dt.isSygus() ){ Node f = n.getOperator(); - Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl; if( n[0].getKind()!=APPLY_CONSTRUCTOR ){ - d_evals[n[0]].push_back( n ); - TypeNode tn = n[0].getType(); - Assert( tn.isDatatype() ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Node var_list = Node::fromExpr( dt.getSygusVarList() ); - Assert( dt.isSygus() ); - d_eval_args[n[0]].push_back( std::vector< Node >() ); - bool isConst = true; - for( unsigned j=1; j<n.getNumChildren(); j++ ){ - d_eval_args[n[0]].back().push_back( n[j] ); - if( !n[j].isConst() ){ - isConst = false; + if (d_eval_processed.find(n) == d_eval_processed.end()) + { + Trace("sygus-eager") + << "TermDbSygus::eager: Register eval term : " << n + << std::endl; + d_eval_processed.insert(n); + d_evals[n[0]].push_back(n); + TypeNode tn = n[0].getType(); + Assert(tn.isDatatype()); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Node var_list = Node::fromExpr(dt.getSygusVarList()); + Assert(dt.isSygus()); + d_eval_args[n[0]].push_back(std::vector<Node>()); + bool isConst = true; + for (unsigned j = 1; j < n.getNumChildren(); j++) + { + d_eval_args[n[0]].back().push_back(n[j]); + if (!n[j].isConst()) + { + isConst = false; + } } + d_eval_args_const[n[0]].push_back(isConst); + Node a = getAnchor(n[0]); + d_subterms[a][n[0]] = true; } - d_eval_args_const[n[0]].push_back( isConst ); - Node a = getAnchor( n[0] ); - d_subterms[a][n[0]] = true; } } } diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h index c819bc781..4786f053b 100644 --- a/src/theory/quantifiers/term_database_sygus.h +++ b/src/theory/quantifiers/term_database_sygus.h @@ -17,6 +17,8 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H +#include <unordered_set> + #include "theory/quantifiers/sygus_explain.h" #include "theory/quantifiers/term_database.h" @@ -243,6 +245,8 @@ public: // for symmetry breaking //for eager instantiation // TODO (as part of #1235) move some of these functions to sygus_explain.h private: + /** the set of evaluation terms we have already processed */ + std::unordered_set<Node, NodeHashFunction> d_eval_processed; std::map< Node, std::map< Node, bool > > d_subterms; std::map< Node, std::vector< Node > > d_evals; std::map< Node, std::vector< std::vector< Node > > > d_eval_args; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ac0de29e3..f6b920cda 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -854,10 +854,21 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within std::set< Node > added; d_term_db->addTerm(n, added, withinQuant, withinInstClosure); - //added contains also the Node that just have been asserted in this branch - if( d_quant_rel ){ - for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){ - if( !withinQuant ){ + if (!withinQuant) + { + if (d_sygus_tdb) + { + d_sygus_tdb->registerEvalTerm(n); + } + + // added contains also the Node that just have been asserted in this + // branch + if (d_quant_rel) + { + for (std::set<Node>::iterator i = added.begin(), end = added.end(); + i != end; + i++) + { d_quant_rel->setRelevance( i->getOperator(), 0 ); } } |