summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/lfsc_checker/check.cpp2
-rw-r--r--proofs/lfsc_checker/expr.cpp2
-rw-r--r--proofs/lfsc_checker/expr.h45
-rw-r--r--proofs/lfsc_checker/main.cpp1
-rw-r--r--proofs/signatures/th_bv_bitblast.plf38
-rw-r--r--src/options/options_handler.cpp34
-rw-r--r--src/options/quantifiers_modes.cpp11
-rw-r--r--src/options/quantifiers_modes.h10
-rw-r--r--src/options/quantifiers_options2
-rw-r--r--src/parser/smt2/Smt2.g13
-rw-r--r--src/parser/smt2/smt2.cpp2
-rw-r--r--src/theory/quantifiers/conjecture_generator.cpp9
-rw-r--r--src/theory/quantifiers/inst_propagator.cpp90
-rw-r--r--src/theory/quantifiers/inst_propagator.h10
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.cpp19
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp187
-rw-r--r--src/theory/quantifiers/quant_conflict_find.h9
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp6
-rw-r--r--src/theory/quantifiers/term_database.cpp171
-rw-r--r--src/theory/quantifiers/term_database.h4
-rw-r--r--src/theory/quantifiers_engine.cpp32
-rw-r--r--src/theory/quantifiers_engine.h1
-rw-r--r--test/regress/regress0/sygus/Makefile.am3
-rw-r--r--test/regress/regress0/sygus/strings-small.sy35
24 files changed, 491 insertions, 245 deletions
diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
index c96791aeb..22e326cda 100644
--- a/proofs/lfsc_checker/check.cpp
+++ b/proofs/lfsc_checker/check.cpp
@@ -24,7 +24,7 @@ int colnum = 1;
const char *filename = 0;
FILE *curfile = 0;
-//#define USE_HASH_MAPS
+//#define USE_HASH_MAPS //AJR: deprecated
symmap2 progs;
std::vector< Expr* > ascHoles;
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
index ae0e49531..5cb774fbf 100644
--- a/proofs/lfsc_checker/expr.cpp
+++ b/proofs/lfsc_checker/expr.cpp
@@ -34,7 +34,6 @@ bool destroy_progs = false;
Expr *r = rr; \
int ref = r->data >> 9; \
ref = ref - 1; \
- r->debugrefcnt(ref,DEC); \
if (ref == 0) { \
_e = r; \
goto start_destroy; \
@@ -43,6 +42,7 @@ bool destroy_progs = false;
r->data = (ref << 9) | (r->data & 511); \
} while(0)
+//removed from below "ref = ref -1;": r->debugrefcnt(ref,DEC);
void Expr::destroy(Expr *_e, bool dec_kids) {
start_destroy:
diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h
index 32a62ab33..5a505a3d9 100644
--- a/proofs/lfsc_checker/expr.h
+++ b/proofs/lfsc_checker/expr.h
@@ -8,9 +8,9 @@
#include <map>
#include "chunking_memory_management.h"
-#define USE_FLAT_APP
+#define USE_FLAT_APP //AJR: off deprecated
#define MARKVAR_32
-#define DEBUG_SYM_NAMES
+//#define DEBUG_SYM_NAMES
//#define DEBUG_SYMS
// Expr class
@@ -66,7 +66,6 @@ protected:
enum { INC, DEC, CREATE };
void debugrefcnt(int ref, int what) {
-#ifdef DEBUG_REFCNT
std::cout << "[";
debug();
switch(what) {
@@ -83,10 +82,6 @@ protected:
char tmp[10];
sprintf(tmp,"%d",ref);
std::cout << tmp << "]\n";
-#else
- (void)ref;
- (void)what;
-#endif
}
Expr(int _class, int _op)
@@ -114,14 +109,18 @@ public:
// std::cout << " " << ref << std::endl;
//}
ref = ref<4194303 ? ref + 1 : ref;
+#ifdef DEBUG_REFCNT
debugrefcnt(ref,INC);
+#endif
data = (ref << 9) | (data & 511);
}
static void destroy(Expr *, bool);
inline void dec(bool dec_kids = true) {
int ref = getrefcnt();
ref = ref - 1;
+#ifdef DEBUG_REFCNT
debugrefcnt(ref,DEC);
+#endif
if (ref == 0)
destroy(this,dec_kids);
else
@@ -131,10 +130,10 @@ public:
//must pass statType (the expr representing "type") to this function
bool isType( Expr* statType );
- inline bool isDatatype() {
+ inline bool isDatatype() const {
return getclass() == SYMS_EXPR || getop() == MPZ || getop() == MPQ;
}
- inline bool isArithTerm() {
+ inline bool isArithTerm() const {
return getop() == ADD || getop() == NEG;
}
@@ -188,13 +187,17 @@ public:
CExpr(int _op) : Expr(CEXPR, _op), kids() {
kids = new Expr *[1];
kids[0] = 0;
+#ifdef DEBUG_REFCNT
debugrefcnt(1,CREATE);
+#endif
}
CExpr(int _op, Expr *e1) : Expr(CEXPR, _op), kids() {
kids = new Expr *[2];
kids[0] = e1;
kids[1] = 0;
+#ifdef DEBUG_REFCNT
debugrefcnt(1,CREATE);
+#endif
}
CExpr(int _op, Expr *e1, Expr *e2)
: Expr(CEXPR, _op), kids() {
@@ -202,7 +205,9 @@ public:
kids[0] = e1;
kids[1] = e2;
kids[2] = 0;
+#ifdef DEBUG_REFCNT
debugrefcnt(1,CREATE);
+#endif
}
CExpr(int _op, Expr *e1, Expr *e2, Expr *e3)
: Expr(CEXPR, _op), kids() {
@@ -211,7 +216,9 @@ public:
kids[1] = e2;
kids[2] = e3;
kids[3] = 0;
+#ifdef DEBUG_REFCNT
debugrefcnt(1,CREATE);
+#endif
}
CExpr(int _op, Expr *e1, Expr *e2, Expr *e3, Expr *e4)
: Expr(CEXPR, _op), kids() {
@@ -221,7 +228,9 @@ public:
kids[2] = e3;
kids[3] = e4;
kids[4] = 0;
+#ifdef DEBUG_REFCNT
debugrefcnt(1,CREATE);
+#endif
}
CExpr(int _op, const std::vector<Expr *> &_kids)
: Expr(CEXPR, _op), kids() {
@@ -230,13 +239,17 @@ public:
for (i = 0; i < iend; i++)
kids[i] = _kids[i];
kids[i] = 0;
+#ifdef DEBUG_REFCNT
debugrefcnt(1,CREATE);
+#endif
}
// _kids must be null-terminated.
CExpr(int _op, bool dummy, Expr **_kids) : Expr(CEXPR, _op), kids(_kids) {
(void)dummy;
+#ifdef DEBUG_REFCNT
debugrefcnt(1,CREATE);
+#endif
}
Expr *whr();
@@ -253,7 +266,9 @@ class IntExpr : public Expr {
}
IntExpr(mpz_t _n) : Expr(INT_EXPR, 0), n() {
mpz_init_set(n,_n);
+#ifdef DEBUG_REFCNT
debugrefcnt(1,CREATE);
+#endif
}
IntExpr(signed long int _n ) : Expr(INT_EXPR, 0), n() {
mpz_init_set_si( n, _n );
@@ -271,7 +286,9 @@ class RatExpr : public Expr {
RatExpr(mpq_t _n) : Expr(RAT_EXPR, 0), n() {
mpq_init( n );
mpq_set(n,_n);
+#ifdef DEBUG_REFCNT
debugrefcnt(1,CREATE);
+#endif
mpq_canonicalize( n );
}
RatExpr(signed long int _n1, unsigned long int _n2 ) : Expr(RAT_EXPR, 0), n() {
@@ -290,15 +307,19 @@ class SymExpr : public Expr {
: Expr(theclass, 0), val(0)
{
(void)_s;
+#ifdef DEBUG_REFCNT
if (theclass == SYM_EXPR)
debugrefcnt(1,CREATE);
+#endif
}
SymExpr(const SymExpr &e, int theclass = SYM_EXPR)
: Expr(theclass, 0), val(0)
{
(void)e;
+#ifdef DEBUG_REFCNT
if (theclass == SYM_EXPR)
debugrefcnt(1,CREATE);
+#endif
}
#ifdef MARKVAR_32
private:
@@ -317,12 +338,16 @@ class SymSExpr : public SymExpr {
SymSExpr(std::string _s, int theclass = SYMS_EXPR)
: SymExpr(_s, theclass), s(_s)
{
+#ifdef DEBUG_REFCNT
debugrefcnt(1,CREATE);
+#endif
}
SymSExpr(const SymSExpr &e, int theclass = SYMS_EXPR)
: SymExpr(e, theclass), s(e.s)
{
+#ifdef DEBUG_REFCNT
debugrefcnt(1,CREATE);
+#endif
}
};
@@ -338,7 +363,9 @@ public:
#ifdef DEBUG_HOLE_NAMES
id = next_id++;
#endif
+#ifdef DEBUG_REFCNT
debugrefcnt(1,CREATE);
+#endif
}
Expr *val; // may be set during subst(), defeq(), and clone().
};
diff --git a/proofs/lfsc_checker/main.cpp b/proofs/lfsc_checker/main.cpp
index 80f36e69f..1d8ba5809 100644
--- a/proofs/lfsc_checker/main.cpp
+++ b/proofs/lfsc_checker/main.cpp
@@ -133,6 +133,7 @@ int main(int argc, char **argv) {
a.files.clear();
#endif
+ std::cout << "Proof checked successfully!" << std::endl << std::endl;
std::cout << "time = " << (int)clock() - check_time << std::endl;
std::cout << "sym count = " << SymExpr::symmCount << std::endl;
std::cout << "marked count = " << Expr::markedCount << std::endl;
diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf
index 8e8c51857..580b54418 100644
--- a/proofs/signatures/th_bv_bitblast.plf
+++ b/proofs/signatures/th_bv_bitblast.plf
@@ -280,7 +280,34 @@
(bbltn (fail bblt))
((bbltc bi b') (bbltc (xor (xor ai bi) (bblast_bvadd_carry a' b' carry))
(bblast_bvadd a' b' carry)))))))
-
+
+
+(program reverse_help ((x bblt) (acc bblt)) bblt
+(match x
+ (bbltn acc)
+ ((bbltc xi x') (reverse_help x' (bbltc xi acc)))))
+
+
+(program reverseb ((x bblt)) bblt
+ (reverse_help x bbltn))
+
+
+; AJR: use this version?
+;(program bblast_bvadd_2h ((a bblt) (b bblt) (carry formula)) bblt
+;(match a
+; ( bbltn (match b (bbltn bbltn) (default (fail bblt))))
+; ((bbltc ai a') (match b
+; (bbltn (fail bblt))
+; ((bbltc bi b')
+; (let carry' (or (and ai bi) (and (xor ai bi) carry))
+; (bbltc (xor (xor ai bi) carry)
+; (bblast_bvadd_2h a' b' carry'))))))))
+
+;(program bblast_bvadd_2 ((a bblt) (b bblt) (carry formula)) bblt
+;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit
+;(let br (reverseb b) ;; from the least significant bit up
+;(let ret (bblast_bvadd_2h ar br carry)
+; (reverseb ret)))))
(declare bv_bbl_bvadd (! n mpz
(! x (term (BitVec n))
@@ -322,15 +349,6 @@
;; shift add multiplier
-(program reverse_help ((x bblt) (acc bblt)) bblt
-(match x
- (bbltn acc)
- ((bbltc xi x') (reverse_help x' (bbltc xi acc)))))
-
-
-(program reverseb ((x bblt)) bblt
- (reverse_help x bbltn))
-
;; (program concat ((a bblt) (b bblt)) bblt
;; (match a (bbltn b)
;; ((bbltc ai a') (bbltc ai (concat a' b)))))
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index a2809bd67..7d41ae862 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -254,15 +254,21 @@ last-call\n\
const std::string OptionsHandler::s_literalMatchHelp = "\
Literal match modes currently supported by the --literal-match option:\n\
\n\
-none (default)\n\
+none \n\
+ Do not use literal matching.\n\
\n\
-predicate\n\
-+ Consider the phase requirements of predicate literals when applying heuristic\n\
- quantifier instantiation. For example, the trigger P( x ) in the quantified \n\
- formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\
- terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\
- Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\
+use (default)\n\
++ Consider phase requirements of triggers conservatively. For example, the\n\
+ trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with\n\
+ terms in the equivalence class of true, and likewise Q( x ) will not be matched\n\
+ terms in the equivalence class of false. Extends to equality.\n\
+\n\
+agg-predicate \n\
++ Consider phase requirements aggressively for predicates. In the above example,\n\
+ only match P( x ) with terms that are in the equivalence class of false.\n\
+\n\
+agg \n\
++ Consider the phase requirements aggressively for all triggers.\n\
\n\
";
@@ -506,10 +512,12 @@ void OptionsHandler::checkInstWhenMode(std::string option, theory::quantifiers::
theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) {
if(optarg == "none") {
return theory::quantifiers::LITERAL_MATCH_NONE;
- } else if(optarg == "predicate") {
- return theory::quantifiers::LITERAL_MATCH_PREDICATE;
- } else if(optarg == "equality") {
- return theory::quantifiers::LITERAL_MATCH_EQUALITY;
+ } else if(optarg == "use") {
+ return theory::quantifiers::LITERAL_MATCH_USE;
+ } else if(optarg == "agg-predicate") {
+ return theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE;
+ } else if(optarg == "agg") {
+ return theory::quantifiers::LITERAL_MATCH_AGG;
} else if(optarg == "help") {
puts(s_literalMatchHelp.c_str());
exit(1);
@@ -520,9 +528,7 @@ theory::quantifiers::LiteralMatchMode OptionsHandler::stringToLiteralMatchMode(s
}
void OptionsHandler::checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) {
- if(mode == theory::quantifiers::LITERAL_MATCH_EQUALITY) {
- throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release.");
- }
+
}
theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) {
diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp
index a58120974..e2cd78de5 100644
--- a/src/options/quantifiers_modes.cpp
+++ b/src/options/quantifiers_modes.cpp
@@ -46,11 +46,14 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMod
case theory::quantifiers::LITERAL_MATCH_NONE:
out << "LITERAL_MATCH_NONE";
break;
- case theory::quantifiers::LITERAL_MATCH_PREDICATE:
- out << "LITERAL_MATCH_PREDICATE";
+ case theory::quantifiers::LITERAL_MATCH_USE:
+ out << "LITERAL_MATCH_USE";
break;
- case theory::quantifiers::LITERAL_MATCH_EQUALITY:
- out << "LITERAL_MATCH_EQUALITY";
+ case theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE:
+ out << "LITERAL_MATCH_AGG_PREDICATE";
+ break;
+ case theory::quantifiers::LITERAL_MATCH_AGG:
+ out << "LITERAL_MATCH_AGG";
break;
default:
out << "LiteralMatchMode!UNKNOWN";
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 5749da972..b4b9abdaf 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -44,10 +44,12 @@ enum InstWhenMode {
enum LiteralMatchMode {
/** Do not consider polarity of patterns */
LITERAL_MATCH_NONE,
- /** Consider polarity of boolean predicates only */
- LITERAL_MATCH_PREDICATE,
- /** Consider polarity of boolean predicates, as well as equalities */
- LITERAL_MATCH_EQUALITY,
+ /** Conservatively consider polarity of patterns */
+ LITERAL_MATCH_USE,
+ /** Aggressively consider polarity of Boolean predicates */
+ LITERAL_MATCH_AGG_PREDICATE,
+ /** Aggressively consider polarity of all terms */
+ LITERAL_MATCH_AGG,
};
enum MbqiMode {
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index f69a8df8b..9fef0295e 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -120,7 +120,7 @@ option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
option fullSaturateInst --fs-inst bool :default false
interleave full saturate instantiation with other techniques
-option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode
+option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_USE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode
choose literal matching mode
### finite model finding options
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 38163c579..c28d23eac 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -760,7 +760,9 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
body = EXPR_MANAGER->mkExpr(kind::EXISTS, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusVars()), body);
Debug("parser-sygus") << "...constructed exists " << body << std::endl;
}
- body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr);
+ if( !PARSER_STATE->getSygusFunSymbols().empty() ){
+ body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr);
+ }
Debug("parser-sygus") << "...constructed forall " << body << std::endl;
Command* c = new SetUserAttributeCommand("sygus", sygusVar);
c->setMuted(true);
@@ -791,6 +793,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
std::string sname;
std::vector< Expr > let_vars;
bool readingLet = false;
+ std::string s;
}
: LPAREN_TOK
//read operator
@@ -890,6 +893,12 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
sgt.d_name = AntlrInput::tokenText($BINARY_LITERAL);
sgt.d_gterm_type = SygusGTerm::gterm_op;
}
+ | str[s,false]
+ { Debug("parser-sygus") << "Sygus grammar " << fun << " : string literal \"" << s << "\"" << std::endl;
+ sgt.d_expr = MK_CONST( ::CVC4::String(s) );
+ sgt.d_name = s;
+ sgt.d_gterm_type = SygusGTerm::gterm_op;
+ }
| symbol[name,CHECK_NONE,SYM_VARIABLE] ( SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { readEnum = true; } )?
{ if( readEnum ){
name = name + "__Enum__" + name2;
@@ -2773,7 +2782,7 @@ STRING_LITERAL_2_0
* will be part of the token text. Use the str[] parser rule instead.
*/
STRING_LITERAL_2_5
- : { PARSER_STATE->v2_5() }?=>
+ : { PARSER_STATE->v2_5() || PARSER_STATE->sygus() }?=>
'"' (~('"') | '""')* '"'
;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index ebad90583..2da44152a 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -350,6 +350,8 @@ void Smt2::setLogic(std::string name) {
name = "UFLIRA";
} else if(name == "BV") {
name = "UFBV";
+ } else if(name == "SLIA") {
+ name = "UFSLIA";
} else if(name == "ALL_SUPPORTED") {
//no change
} else {
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index fa71f0132..f4eb67d74 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1572,7 +1572,6 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode,
if( d_match_status_child_num==0 ){
//initial binding
TNode f = s->getTgFunc( d_typ, d_status_num );
- //std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc );
Assert( !eqc.isNull() );
TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f );
if( tat ){
@@ -1726,9 +1725,9 @@ void TermGenEnv::collectSignatureInformation() {
d_func_kind.clear();
d_func_args.clear();
TypeNode tnull;
- for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){
- if( getTermDatabase()->getNumGroundTerms( it->first )>0 ){
- Node nn = getTermDatabase()->getGroundTerm( it->first, 0 );
+ for( std::map< Node, std::vector< Node > >::iterator it = getTermDatabase()->d_op_map.begin(); it != getTermDatabase()->d_op_map.end(); ++it ){
+ if( !it->second.empty() ){
+ Node nn = it->second[0];
Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl;
if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
bool do_enum = true;
@@ -1750,7 +1749,7 @@ void TermGenEnv::collectSignatureInformation() {
d_typ_tg_funcs[nn.getType()].push_back( it->first );
d_tg_func_param[it->first] = ( nn.getMetaKind() == kind::metakind::PARAMETERIZED );
Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl;
- getTermDatabase()->computeUfEqcTerms( it->first );
+ //getTermDatabase()->computeUfEqcTerms( it->first );
}
}
Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl;
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 1dc6f6d50..41c9c40c8 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -34,6 +34,7 @@ bool EqualityQueryInstProp::reset( Theory::Effort e ) {
d_uf.clear();
d_uf_exp.clear();
d_diseq_list.clear();
+ d_uf_func_map_trie.clear();
return true;
}
@@ -103,7 +104,7 @@ TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& arg
if( !t.isNull() ){
return t;
}else{
- return d_func_map_trie[f].existsTerm( args );
+ return d_uf_func_map_trie[f].existsTerm( args );
}
}
@@ -168,6 +169,21 @@ bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >&
}
}
+TNode EqualityQueryInstProp::getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp ) {
+ TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );
+ if( !t.isNull() ){
+ return t;
+ }else{
+ TNode tt = d_uf_func_map_trie[f].existsTerm( args );
+ if( !tt.isNull() ){
+ //TODO?
+ return tt;
+ }else{
+ return tt;
+ }
+ }
+}
+
Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) {
Assert( exp.empty() );
std::map< Node, Node >::iterator it = d_uf.find( a );
@@ -279,11 +295,13 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
Assert( d_uf_exp[ar].empty() );
Assert( d_uf_exp[br].empty() );
+ //registerUfTerm( ar );
d_uf[ar] = br;
merge_exp( d_uf_exp[ar], exp_a );
merge_exp( d_uf_exp[ar], exp_b );
merge_exp( d_uf_exp[ar], reason );
+ //registerUfTerm( br );
d_uf[br] = br;
d_uf_exp[br].clear();
@@ -316,6 +334,25 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
}
}
+void EqualityQueryInstProp::registerUfTerm( TNode n ) {
+ if( d_uf.find( n )==d_uf.end() ){
+ if( !getEngine()->hasTerm( n ) ){
+ TNode f = d_qe->getTermDatabase()->getMatchOperator( n );
+ if( !f.isNull() ){
+ std::vector< TNode > args;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !getEngine()->hasTerm( n[i] ) ){
+ return;
+ }else{
+ args.push_back( n[i] );
+ }
+ }
+ d_uf_func_map_trie[f].addTerm( n, args );
+ }
+ }
+ }
+}
+
//void EqualityQueryInstProp::addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ) {
void EqualityQueryInstProp::addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch ) {
if( is_watch ){
@@ -573,6 +610,7 @@ bool InstPropagator::reset( Theory::Effort e ) {
d_watch_list.clear();
d_update_list.clear();
d_relevant_inst.clear();
+ d_has_relevant_inst = false;
return d_qy.reset( e );
}
@@ -607,7 +645,31 @@ bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, st
return !d_conflict;
}else{
Assert( false );
- return true;
+ return false;
+ }
+}
+
+void InstPropagator::filterInstantiations() {
+ if( d_has_relevant_inst ){
+ //now, inform quantifiers engine which instances should be retracted
+ Trace("qip-prop-debug") << "...remove instantiation ids : ";
+ for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){
+ if( !it->second.d_q.isNull() ){
+ if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){
+ if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){
+ Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
+ Assert( false );
+ }else{
+ Trace("qip-prop-debug") << it->first << " ";
+ }
+ }else{
+ //mark the quantified formula as relevant
+ d_qe->markRelevant( it->second.d_q );
+ }
+ }
+ }
+ Trace("qip-prop-debug") << std::endl;
+ Trace("quant-engine-conflict") << "-----> InstPropagator::" << ( d_conflict ? "conflict" : "propagate" ) << " with " << d_relevant_inst.size() << " instances." << std::endl;
}
}
@@ -720,10 +782,12 @@ void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& e
}
if( pol ){
if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){
+ Trace("qip-rlv-propagate") << "Relevant propagation : " << a << ( pol ? " == " : " != " ) << b << std::endl;
Assert( d_qy.getEngine()->hasTerm( a ) );
Assert( d_qy.getEngine()->hasTerm( b ) );
Trace("qip-prop-debug") << "...equality between known terms." << std::endl;
addRelevantInstances( exp, "qip-propagate" );
+ //d_has_relevant_inst = true;
}
Trace("qip-prop-debug") << "...merged representatives " << a << " and " << b << std::endl;
for( unsigned i=0; i<2; i++ ){
@@ -750,27 +814,7 @@ void InstPropagator::conflict( std::vector< Node >& exp ) {
d_conflict = true;
d_relevant_inst.clear();
addRelevantInstances( exp, "qip-propagate" );
-
- //now, inform quantifiers engine which instances should be retracted
- Trace("qip-prop-debug") << "...remove instantiation ids : ";
- for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){
- if( !it->second.d_q.isNull() ){
- if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){
- if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){
- Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
- Assert( false );
- }else{
- Trace("qip-prop-debug") << it->first << " ";
- }
- }else{
- //mark the quantified formula as relevant
- d_qe->markRelevant( it->second.d_q );
- }
- }
- }
- Trace("qip-prop-debug") << std::endl;
- //will interupt the quantifiers engine
- Trace("quant-engine-conflict") << "-----> InstPropagator::conflict with " << exp.size() << " instances." << std::endl;
+ d_has_relevant_inst = true;
}
bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index 61aa8257f..6201cf152 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -64,9 +64,11 @@ public:
bool areEqualExp( Node a, Node b, std::vector< Node >& exp );
/** returns true is a and b are disequal in the current context */
bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );
+ /** get congruent term */
+ TNode getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp );
private:
/** term index */
- std::map< Node, TermArgTrie > d_func_map_trie;
+ std::map< Node, TermArgTrie > d_uf_func_map_trie;
/** union find for terms beyond what is stored in equality engine */
std::map< Node, Node > d_uf;
std::map< Node, std::vector< Node > > d_uf_exp;
@@ -75,6 +77,8 @@ private:
std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list;
/** add arg */
void addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch );
+ /** register term */
+ void registerUfTerm( TNode n );
public:
enum {
STATUS_CONFLICT,
@@ -110,10 +114,13 @@ private:
virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
return d_ip.notifyInstantiation( quant_e, q, lem, terms, body );
}
+ virtual void filterInstantiations() { d_ip.filterInstantiations(); }
};
InstantiationNotifyInstPropagator d_notify;
/** notify instantiation method */
bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );
+ /** remove instance ids */
+ void filterInstantiations();
/** allocate instantiation */
unsigned allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body );
/** equality query */
@@ -142,6 +149,7 @@ private:
std::vector< unsigned > d_update_list;
/** relevant instances */
std::map< unsigned, bool > d_relevant_inst;
+ bool d_has_relevant_inst;
private:
bool update( unsigned id, InstInfo& i, bool firstTime = false );
void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index d58bbcf3a..7bc51dc50 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -332,19 +332,30 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
unsigned num_fv = tinfo[pat].d_fv.size();
Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl;
if( rpol!=0 ){
+ Assert( rpol==1 || rpol==-1 );
if( Trigger::isRelationalTrigger( pat ) ){
pat = rpol==-1 ? pat.negate() : pat;
}else{
Assert( Trigger::isAtomicTrigger( pat ) );
if( pat.getType().isBoolean() && rpoleq.isNull() ){
- pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
+ if( options::literalMatchMode()==LITERAL_MATCH_USE ){
+ pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
+ }else if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
+ pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==1 ) );
+ }
}else{
Assert( !rpoleq.isNull() );
if( rpol==-1 ){
- //all equivalence classes except rpoleq
- pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate();
+ if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
+ //all equivalence classes except rpoleq
+ pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate();
+ }
}else if( rpol==1 ){
- //all equivalence classes that are not disequal to rpoleq TODO
+ if( options::literalMatchMode()==LITERAL_MATCH_AGG ){
+ //only equivalence class rpoleq
+ pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq );
+ }
+ //all equivalence classes that are not disequal to rpoleq TODO?
}
}
}
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 52563978f..1365feda9 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -119,7 +119,7 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
//}
//get all variables that are always relevant
std::map< TNode, bool > visited;
- getPropagateVars( vars, q[1], false, visited );
+ getPropagateVars( p, vars, q[1], false, visited );
for( unsigned j=0; j<vars.size(); j++ ){
Node v = vars[j];
TNode f = p->getTermDatabase()->getMatchOperator( v );
@@ -140,7 +140,7 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
}
}
-void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){
+void QuantInfo::getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){
std::map< TNode, bool >::iterator itv = visited.find( n );
if( itv==visited.end() ){
visited[n] = true;
@@ -149,6 +149,12 @@ void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol,
if( d_var_num.find( n )!=d_var_num.end() ){
Assert( std::find( vars.begin(), vars.end(), n )==vars.end() );
vars.push_back( n );
+ TNode f = p->getTermDatabase()->getMatchOperator( n );
+ if( !f.isNull() ){
+ if( std::find( p->d_func_rel_dom[f].begin(), p->d_func_rel_dom[f].end(), d_q )==p->d_func_rel_dom[f].end() ){
+ p->d_func_rel_dom[f].push_back( d_q );
+ }
+ }
}else if( MatchGen::isHandledBoolConnective( n ) ){
Assert( n.getKind()!=IMPLIES );
QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol );
@@ -156,7 +162,7 @@ void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol,
Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl;
if( rec ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- getPropagateVars( vars, n[i], pol, visited );
+ getPropagateVars( p, vars, n[i], pol, visited );
}
}
}
@@ -238,7 +244,7 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) {
}
-void QuantInfo::reset_round( QuantConflictFind * p ) {
+bool QuantInfo::reset_round( QuantConflictFind * p ) {
for( unsigned i=0; i<d_match.size(); i++ ){
d_match[i] = TNode::null();
d_match_term[i] = TNode::null();
@@ -246,6 +252,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) {
d_vars_set.clear();
d_curr_var_deq.clear();
d_tconstraints.clear();
+
//add built-in variable constraints
for( unsigned r=0; r<2; r++ ){
for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();
@@ -263,7 +270,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) {
d_mg->d_children.clear();
d_mg->d_n = NodeManager::currentNM()->mkConst( true );
d_mg->d_type = MatchGen::typ_ground;
- return;
+ return false;
}
}
}
@@ -274,6 +281,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) {
}
//now, reset for matching
d_mg->reset( p, false, this );
+ return true;
}
int QuantInfo::getCurrentRepVar( int v ) {
@@ -1283,11 +1291,14 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
}
}else if( d_type==typ_var ){
Assert( isHandledUfTerm( d_n ) );
- Node f = getMatchOperator( p, d_n );
+ TNode f = getMatchOperator( p, d_n );
Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl;
TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f );
if( qni!=NULL ){
d_qn.push_back( qni );
+ }else{
+ //inform irrelevant quantifiers
+ p->setIrrelevantFunction( f );
}
d_matched_basis = false;
}else if( d_type==typ_tsym || d_type==typ_tconstraint ){
@@ -2013,6 +2024,18 @@ void QuantConflictFind::reset_round( Theory::Effort level ) {
d_needs_computeRelEqr = true;
}
+void QuantConflictFind::setIrrelevantFunction( TNode f ) {
+ if( d_irr_func.find( f )==d_irr_func.end() ){
+ d_irr_func[f] = true;
+ std::map< TNode, std::vector< Node > >::iterator it = d_func_rel_dom.find( f );
+ if( it != d_func_rel_dom.end()){
+ for( unsigned j=0; j<it->second.size(); j++ ){
+ d_irr_quant[it->second[j]] = true;
+ }
+ }
+ }
+}
+
/** check */
void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
@@ -2035,14 +2058,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
}
computeRelevantEqr();
- //determine order for quantified formulas
- std::vector< Node > qorder;
- for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
- Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
- if( d_quantEngine->hasOwnership( q, this ) ){
- qorder.push_back( q );
- }
- }
+ d_irr_func.clear();
+ d_irr_quant.clear();
+
if( Trace.isOn("qcf-debug") ){
Trace("qcf-debug") << std::endl;
debugPrint("qcf-debug");
@@ -2053,80 +2071,83 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
for( short e = effort_conflict; e<=end_e; e++ ){
d_effort = e;
Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
- for( unsigned j=0; j<qorder.size(); j++ ){
- Node q = qorder[j];
- QuantInfo * qi = &d_qinfo[q];
-
- Assert( d_qinfo.find( q )!=d_qinfo.end() );
- if( qi->matchGeneratorIsValid() ){
- Trace("qcf-check") << "Check quantified formula ";
- debugPrintQuant("qcf-check", q);
- Trace("qcf-check") << " : " << q << "..." << std::endl;
-
- Trace("qcf-check-debug") << "Reset round..." << std::endl;
- qi->reset_round( this );
- //try to make a matches making the body false
- Trace("qcf-check-debug") << "Get next match..." << std::endl;
- while( qi->getNextMatch( this ) ){
- Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
- qi->debugPrintMatch("qcf-inst");
- Trace("qcf-inst") << std::endl;
- if( !qi->isMatchSpurious( this ) ){
- std::vector< int > assigned;
- if( qi->completeMatch( this, assigned ) ){
- std::vector< Node > terms;
- qi->getMatch( terms );
- bool tcs = qi->isTConstraintSpurious( this, terms );
- if( !tcs ){
- //for debugging
- if( Debug.isOn("qcf-check-inst") ){
- Node inst = d_quantEngine->getInstantiation( q, terms );
- Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
- Assert( !getTermDatabase()->isEntailed( inst, true ) );
- Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict );
- }
- if( d_quantEngine->addInstantiation( q, terms ) ){
- Trace("qcf-check") << " ... Added instantiation" << std::endl;
- Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
- qi->debugPrintMatch("qcf-inst");
- Trace("qcf-inst") << std::endl;
- ++addedLemmas;
- if( e==effort_conflict ){
- d_quantEngine->markRelevant( q );
- ++(d_statistics.d_conflict_inst);
- if( options::qcfAllConflict() ){
- isConflict = true;
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
+ if( d_quantEngine->hasOwnership( q, this ) && d_irr_quant.find( q )==d_irr_quant.end() ){
+ QuantInfo * qi = &d_qinfo[q];
+
+ Assert( d_qinfo.find( q )!=d_qinfo.end() );
+ if( qi->matchGeneratorIsValid() ){
+ Trace("qcf-check") << "Check quantified formula ";
+ debugPrintQuant("qcf-check", q);
+ Trace("qcf-check") << " : " << q << "..." << std::endl;
+
+ Trace("qcf-check-debug") << "Reset round..." << std::endl;
+ if( qi->reset_round( this ) ){
+ //try to make a matches making the body false
+ Trace("qcf-check-debug") << "Get next match..." << std::endl;
+ while( qi->getNextMatch( this ) ){
+ Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
+ qi->debugPrintMatch("qcf-inst");
+ Trace("qcf-inst") << std::endl;
+ if( !qi->isMatchSpurious( this ) ){
+ std::vector< int > assigned;
+ if( qi->completeMatch( this, assigned ) ){
+ std::vector< Node > terms;
+ qi->getMatch( terms );
+ bool tcs = qi->isTConstraintSpurious( this, terms );
+ if( !tcs ){
+ //for debugging
+ if( Debug.isOn("qcf-check-inst") ){
+ Node inst = d_quantEngine->getInstantiation( q, terms );
+ Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
+ Assert( !getTermDatabase()->isEntailed( inst, true ) );
+ Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict );
+ }
+ if( d_quantEngine->addInstantiation( q, terms ) ){
+ Trace("qcf-check") << " ... Added instantiation" << std::endl;
+ Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
+ qi->debugPrintMatch("qcf-inst");
+ Trace("qcf-inst") << std::endl;
+ ++addedLemmas;
+ if( e==effort_conflict ){
+ d_quantEngine->markRelevant( q );
+ ++(d_statistics.d_conflict_inst);
+ if( options::qcfAllConflict() ){
+ isConflict = true;
+ }else{
+ d_conflict.set( true );
+ }
+ break;
+ }else if( e==effort_prop_eq ){
+ d_quantEngine->markRelevant( q );
+ ++(d_statistics.d_prop_inst);
+ }
}else{
- d_conflict.set( true );
+ Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl;
+ //this should only happen if the algorithm generates the same propagating instance twice this round
+ //in this case, break to avoid exponential behavior
+ break;
}
- break;
- }else if( e==effort_prop_eq ){
- d_quantEngine->markRelevant( q );
- ++(d_statistics.d_prop_inst);
+ }else{
+ Trace("qcf-inst") << " ... Spurious instantiation (match is T-inconsistent)" << std::endl;
}
+ //clean up assigned
+ qi->revertMatch( this, assigned );
+ d_tempCache.clear();
}else{
- Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl;
- //this should only happen if the algorithm generates the same propagating instance twice this round
- //in this case, break to avoid exponential behavior
- break;
+ Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
}
}else{
- Trace("qcf-inst") << " ... Spurious instantiation (match is T-inconsistent)" << std::endl;
+ Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl;
}
- //clean up assigned
- qi->revertMatch( this, assigned );
- d_tempCache.clear();
- }else{
- Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
}
- }else{
- Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl;
+ Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
+ if( d_conflict ){
+ break;
+ }
}
}
- Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
- if( d_conflict ){
- break;
- }
}
}
if( addedLemmas>0 ){
@@ -2157,17 +2178,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
void QuantConflictFind::computeRelevantEqr() {
if( d_needs_computeRelEqr ){
d_needs_computeRelEqr = false;
- Trace("qcf-check") << "Compute relevant equalities..." << std::endl;
- //d_uf_terms.clear();
- //d_eqc_uf_terms.clear();
+ Trace("qcf-check") << "Compute relevant equivalence classes..." << std::endl;
d_eqcs.clear();
- //d_arg_reps.clear();
- //double clSet = 0;
- //if( Trace.isOn("qcf-opt") ){
- // clSet = double(clock())/double(CLOCKS_PER_SEC);
- //}
- //now, store matches
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
while( !eqcs_i.isFinished() ){
Node r = (*eqcs_i);
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 16f6b6a1b..974495269 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -117,7 +117,7 @@ private: //for completing match
std::vector< int > d_una_eqc_count;
//optimization: track which arguments variables appear under UF terms in
std::map< int, std::map< TNode, std::vector< unsigned > > > d_var_rel_dom;
- void getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited );
+ void getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited );
//optimization: number of variables set, to track when we can stop
std::map< int, bool > d_vars_set;
std::map< Node, bool > d_ground_terms;
@@ -156,7 +156,7 @@ public:
}
Node d_q;
- void reset_round( QuantConflictFind * p );
+ bool reset_round( QuantConflictFind * p );
public:
//initialize
void initialize( QuantConflictFind * p, Node q, Node qn );
@@ -195,6 +195,11 @@ private:
std::map< Kind, Node > d_zero;
//for storing nodes created during t-constraint solving (prevents memory leaks)
std::vector< Node > d_tempCache;
+ //optimization: list of quantifiers that depend on ground function applications
+ std::map< TNode, std::vector< Node > > d_func_rel_dom;
+ std::map< TNode, bool > d_irr_func;
+ std::map< Node, bool > d_irr_quant;
+ void setIrrelevantFunction( TNode f );
private:
std::map< Node, Node > d_op_node;
int d_fid_count;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 2f7864831..6963f7e62 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -187,7 +187,6 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
std::vector< Node > args;
Node body = in;
bool doRewrite = false;
- bool firstTime = true;
while( body.getNumChildren()==2 && body.getKind()==body[1].getKind() ){
for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
args.push_back( body[0][i] );
@@ -197,8 +196,11 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
}
if( doRewrite ){
std::vector< Node > children;
+ for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
+ args.push_back( body[0][i] );
+ }
children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST,args) );
- children.push_back( body );
+ children.push_back( body[1] );
Node n = NodeManager::currentNM()->mkNode( in.getKind(), children );
if( in!=n ){
Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index b143286cc..61c02d3ac 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -163,6 +163,10 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
//if this is an atomic trigger, consider adding it
if( inst::Trigger::isAtomicTrigger( n ) ){
Trace("term-db") << "register term in db " << n << std::endl;
+ if( options::finiteModelFind() ){
+ computeModelBasisArgAttribute( n );
+ }
+
Node op = getMatchOperator( n );
d_op_map[op].push_back( n );
added.insert( n );
@@ -222,7 +226,86 @@ void TermDb::computeUfEqcTerms( TNode f ) {
}
}
+void TermDb::computeUfTerms( TNode f ) {
+ if( d_op_nonred_count.find( f )==d_op_nonred_count.end() ){
+ d_op_nonred_count[ f ] = 0;
+ std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f );
+ if( it!=d_op_map.end() ){
+ eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+ Trace("term-db-debug") << "Adding terms for operator " << f << std::endl;
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ Node n = it->second[i];
+ //to be added to term index, term must be relevant, and exist in EE
+ if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
+ if( isTermActive( n ) ){
+ computeArgReps( n );
+
+ Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
+ for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
+ Trace("term-db-debug") << d_arg_reps[n][i] << " ";
+ if( std::find( d_func_map_rel_dom[f][i].begin(),
+ d_func_map_rel_dom[f][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[f][i].end() ){
+ d_func_map_rel_dom[f][i].push_back( d_arg_reps[n][i] );
+ }
+ }
+ Trace("term-db-debug") << std::endl;
+ Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl;
+ Node at = d_func_map_trie[ f ].addOrGetTerm( n, d_arg_reps[n] );
+ Trace("term-db-debug2") << "...add term returned " << at << std::endl;
+ if( at!=n && ee->areEqual( at, n ) ){
+ setTermInactive( n );
+ Trace("term-db-debug") << n << " is redundant." << std::endl;
+ //congruentCount++;
+ }else{
+ if( at!=n && ee->areDisequal( at, n, false ) ){
+ std::vector< Node > lits;
+ lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) );
+ for( unsigned i=0; i<at.getNumChildren(); i++ ){
+ if( at[i]!=n[i] ){
+ lits.push_back( NodeManager::currentNM()->mkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() );
+ }
+ }
+ Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits );
+ if( Trace.isOn("term-db-lemma") ){
+ Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl;
+ if( !d_quantEngine->getTheoryEngine()->needCheck() ){
+ Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl;
+ }
+ Trace("term-db-lemma") << " add lemma : " << lem << std::endl;
+ }
+ d_quantEngine->addLemma( lem );
+ d_consistent_ee = false;
+ return;
+ }
+ //nonCongruentCount++;
+ d_op_nonred_count[ f ]++;
+ }
+ }else{
+ Trace("term-db-debug") << n << " is already redundant." << std::endl;
+ //congruentCount++;
+ //alreadyCongruentCount++;
+ }
+ }else{
+ Trace("term-db-debug") << n << " is not relevant." << std::endl;
+ //nonRelevantCount++;
+ }
+ }
+
+ /*
+ if( Trace.isOn("term-db-index") ){
+ Trace("term-db-index") << "Term index for " << f << " : " << std::endl;
+ Trace("term-db-index") << "- " << it->first << std::endl;
+ d_func_map_trie[ f ].debugPrint("term-db-index", it->second[0]);
+ Trace("term-db-index") << "Non-Congruent/Congruent/Non-Relevant = ";
+ Trace("term-db-index") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl;
+ }
+ */
+ }
+ }
+}
+
bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
+ computeUfTerms( f );
Assert( d_quantEngine->getTheoryEngine()->getMasterEqualityEngine()->getRepresentative( r )==r );
std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
if( it != d_func_map_rel_dom.end() ){
@@ -584,10 +667,10 @@ void TermDb::presolve() {
}
bool TermDb::reset( Theory::Effort effort ){
- int nonCongruentCount = 0;
- int congruentCount = 0;
- int alreadyCongruentCount = 0;
- int nonRelevantCount = 0;
+ //int nonCongruentCount = 0;
+ //int congruentCount = 0;
+ //int alreadyCongruentCount = 0;
+ //int nonRelevantCount = 0;
d_op_nonred_count.clear();
d_arg_reps.clear();
d_func_map_trie.clear();
@@ -642,71 +725,16 @@ bool TermDb::reset( Theory::Effort effort ){
}
}
+/*
//rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
- d_op_nonred_count[ it->first ] = 0;
- Trace("term-db-debug") << "Adding terms for operator " << it->first << std::endl;
- for( unsigned i=0; i<it->second.size(); i++ ){
- Node n = it->second[i];
- //to be added to term index, term must be relevant, and exist in EE
- if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
- if( isTermActive( n ) ){
- if( options::finiteModelFind() ){
- computeModelBasisArgAttribute( n );
- }
- computeArgReps( n );
-
- Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
- for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
- Trace("term-db-debug") << d_arg_reps[n][i] << " ";
- if( std::find( d_func_map_rel_dom[it->first][i].begin(),
- d_func_map_rel_dom[it->first][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[it->first][i].end() ){
- d_func_map_rel_dom[it->first][i].push_back( d_arg_reps[n][i] );
- }
- }
- Trace("term-db-debug") << std::endl;
- Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl;
- Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] );
- Trace("term-db-debug2") << "...add term returned " << at << std::endl;
- if( at!=n && ee->areEqual( at, n ) ){
- setTermInactive( n );
- Trace("term-db-debug") << n << " is redundant." << std::endl;
- congruentCount++;
- }else{
- if( at!=n && ee->areDisequal( at, n, false ) ){
- std::vector< Node > lits;
- lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) );
- for( unsigned i=0; i<at.getNumChildren(); i++ ){
- if( at[i]!=n[i] ){
- lits.push_back( NodeManager::currentNM()->mkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() );
- }
- }
- Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits );
- if( Trace.isOn("term-db-lemma") ){
- Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl;
- if( !d_quantEngine->getTheoryEngine()->needCheck() ){
- Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl;
- }
- Trace("term-db-lemma") << " add lemma : " << lem << std::endl;
- }
- d_quantEngine->addLemma( lem );
- d_consistent_ee = false;
- return false;
- }
- nonCongruentCount++;
- d_op_nonred_count[ it->first ]++;
- }
- }else{
- Trace("term-db-debug") << n << " is already redundant." << std::endl;
- congruentCount++;
- alreadyCongruentCount++;
- }
- }else{
- Trace("term-db-debug") << n << " is not relevant." << std::endl;
- nonRelevantCount++;
- }
+ computeUfTerms( it->first );
+ if( !d_consistent_ee ){
+ return false;
}
}
+*/
+ /*
Trace("term-db-stats") << "TermDb: Reset" << std::endl;
Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = ";
Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl;
@@ -719,10 +747,12 @@ bool TermDb::reset( Theory::Effort effort ){
}
}
}
+ */
return true;
}
TermArgTrie * TermDb::getTermArgTrie( Node f ) {
+ computeUfTerms( f );
std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f );
if( itut!=d_func_map_trie.end() ){
return &itut->second;
@@ -751,11 +781,18 @@ TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) {
}
TNode TermDb::getCongruentTerm( Node f, Node n ) {
- computeArgReps( n );
- return d_func_map_trie[f].existsTerm( d_arg_reps[n] );
+ computeUfTerms( f );
+ std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f );
+ if( itut!=d_func_map_trie.end() ){
+ computeArgReps( n );
+ return itut->second.existsTerm( d_arg_reps[n] );
+ }else{
+ return TNode::null();
+ }
}
TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) {
+ computeUfTerms( f );
return d_func_map_trie[f].existsTerm( args );
}
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 004292622..684b6cf83 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -248,6 +248,8 @@ public:
void computeArgReps( TNode n );
/** compute uf eqc terms */
void computeUfEqcTerms( TNode f );
+ /** compute uf terms */
+ void computeUfTerms( TNode f );
/** in relevant domain */
bool inRelevantDomain( TNode f, unsigned i, TNode r );
/** evaluate a term under a substitution. Return representative in EE if possible.
@@ -271,7 +273,7 @@ public:
Node getEligibleTermInEqc( TNode r );
/** is inst closure */
bool isInstClosure( Node r );
-
+
//for model basis
private:
//map from types to model basis terms
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2451036f1..12edb5277 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -353,7 +353,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
std::vector< QuantifiersModule* > qm;
if( d_model->checkNeeded() ){
needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call
- for( int i=0; i<(int)d_modules.size(); i++ ){
+ for( unsigned i=0; i<d_modules.size(); i++ ){
if( d_modules[i]->needsCheck( e ) ){
qm.push_back( d_modules[i] );
needsCheck = true;
@@ -396,6 +396,12 @@ void QuantifiersEngine::check( Theory::Effort e ){
}
d_recorded_inst.clear();
}
+
+ double clSet = 0;
+ if( Trace.isOn("quant-engine") ){
+ clSet = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e << " <<<<<" << std::endl;
+ }
if( Trace.isOn("quant-engine-debug") ){
Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
@@ -456,7 +462,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
flushLemmas();
if( d_hasAddedLemma ){
return;
-
}
if( e==Theory::EFFORT_LAST_CALL ){
@@ -548,6 +553,13 @@ void QuantifiersEngine::check( Theory::Effort e ){
}
}
}
+ if( Trace.isOn("quant-engine") ){
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet);
+ Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma;
+ Trace("quant-engine") << std::endl;
+ }
+
Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
}else{
Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
@@ -567,7 +579,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
}
}
if( setIncomplete ){
- Trace("quant-engine-debug") << "Set incomplete flag." << std::endl;
+ Trace("quant-engine") << "Set incomplete flag." << std::endl;
getOutputChannel().setIncomplete();
}
//output debug stats
@@ -646,8 +658,6 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
d_modules[i]->registerQuantifier( f );
}
Node ceBody = d_term_db->getInstConstantBody( f );
- //generate the phase requirements
- //d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
//also register it with the strong solver
//if( options::finiteModelFind() ){
// ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
@@ -1209,9 +1219,19 @@ quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() {
void QuantifiersEngine::flushLemmas(){
if( !d_lemmas_waiting.empty() ){
+ //filter based on notify classes
+ if( !d_inst_notify.empty() ){
+ unsigned prev_lem_sz = d_lemmas_waiting.size();
+ for( unsigned j=0; j<d_inst_notify.size(); j++ ){
+ d_inst_notify[j]->filterInstantiations();
+ }
+ if( prev_lem_sz!=d_lemmas_waiting.size() ){
+ Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl;
+ }
+ }
//take default output channel if none is provided
d_hasAddedLemma = true;
- for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){
+ for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
}
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 4c7cb4a2f..60666c4a9 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -48,6 +48,7 @@ class InstantiationNotify {
public:
InstantiationNotify(){}
virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
+ virtual void filterInstantiations() = 0;
};
namespace quantifiers {
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 2ca807662..8c847be60 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -48,7 +48,8 @@ TESTS = commutative.sy \
clock-inc-tuple.sy \
dt-test-ns.sy \
no-mention.sy \
- max2-univ.sy
+ max2-univ.sy \
+ strings-small.sy
# sygus tests currently taking too long for make regress
EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy
new file mode 100644
index 000000000..bc559f94a
--- /dev/null
+++ b/test/regress/regress0/sygus/strings-small.sy
@@ -0,0 +1,35 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si --no-dump-synth
+(set-logic SLIA)
+(synth-fun f ((firstname String) (lastname String)) String
+((Start String (ntString))
+
+(ntString String (
+firstname
+lastname
+" "
+(str.++ ntString ntString)))
+
+(ntInt Int (
+0
+1
+2
+(+ ntInt ntInt)
+(- ntInt ntInt)
+(str.len ntString)
+(str.to.int ntString)
+(str.indexof ntString ntString ntInt)))
+
+(ntBool Bool (
+true
+false
+(str.prefixof ntString ntString)
+(str.suffixof ntString ntString)
+(str.contains ntString ntString)))
+
+))
+
+(constraint (= (f "Nancy" "FreeHafer") "Nancy FreeHafer"))
+
+(check-synth)
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback