From 8b41e8d8128752eba75f32f751ec9c095a6b1d87 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 12 Mar 2014 14:25:25 -0500 Subject: [PATCH] Work on array pf signature, add working example. Add quantifiers proof signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default. --- proofs/signatures/example-arrays.plf | 139 ++++++++++++++++++ proofs/signatures/th_arrays.plf | 29 ++-- proofs/signatures/th_quant.plf | 52 +++++++ .../quantifiers/candidate_generator.cpp | 2 +- src/theory/quantifiers/model_builder.cpp | 2 +- src/theory/quantifiers/options | 2 +- .../quantifiers/quant_conflict_find.cpp | 5 +- src/theory/quantifiers/relevant_domain.cpp | 3 +- src/theory/quantifiers/term_database.cpp | 29 +++- src/theory/quantifiers/term_database.h | 11 +- src/theory/quantifiers_engine.cpp | 2 +- test/regress/regress0/push-pop/bug326.smt2 | 2 +- 12 files changed, 248 insertions(+), 30 deletions(-) create mode 100755 proofs/signatures/example-arrays.plf create mode 100755 proofs/signatures/th_quant.plf diff --git a/proofs/signatures/example-arrays.plf b/proofs/signatures/example-arrays.plf new file mode 100755 index 000000000..600fc11c9 --- /dev/null +++ b/proofs/signatures/example-arrays.plf @@ -0,0 +1,139 @@ +; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf + +; -------------------------------------------------------------------------------- +; literals : +; L1 : a = write( a, i, read( a, i ) +; L2 : read( a, k ) = read( write( a, i, read( a, i ) ), k ) +; L3 : i = k + +; input : +; ~L1 + +; (extenstionality) lemma : +; L1 or ~L2 + +; theory conflicts : +; L2 or ~L3 +; L2 or L3 + + +; With the theory lemma, the input is unsatisfiable. +; -------------------------------------------------------------------------------- + + +; (0) -------------------- term declarations ----------------------------------- + +(check +(% I sort +(% E sort +(% a (term (array I E)) +(% i (term I) + + +; (1) -------------------- input formula ----------------------------------- + +(% A1 (th_holds (not (= (array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))) + + + + +; (2) ------------------- specify that the following is a proof of the empty clause ----------------- + +(: (holds cln) + + + + +; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF ----------------- +; --- these should introduce (th_holds ...) + + +; extensionality lemma : notice this also introduces skolem k +(ext _ _ a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)) (\ k (\ A2 + + + + +; (4) -------------------- map theory literals to boolean variables +; --- maps all theory literals involved in proof to boolean literals + +(decl_atom (= (array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1 +(decl_atom (= E (apply _ _ (apply _ _ (read I E) a) k) (apply _ _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) k)) (\ v2 (\ a2 +(decl_atom (= I i k) (\ v3 (\ a3 + + + +; (5) -------------------- theory conflicts --------------------------------------------- +; --- these should introduce (holds ...) + +(satlem _ _ +(asf _ _ _ a3 (\ l3 +(asf _ _ _ a2 (\ l2 +(clausify_false + + ; use read over write rule "row" + (contra _ (symm _ _ _ (row _ _ _ _ a (apply _ _ (apply _ _ (read I E) a) i) l3)) l2) + +))))) (\ CT1 +; CT1 is the clause ( v2 V v3 ) + +(satlem _ _ +(ast _ _ _ a3 (\ l3 +(asf _ _ _ a2 (\ l2 +(clausify_false + + ; use read over write rule "row1" + (contra _ (symm _ _ _ + (trans _ _ _ _ + (symm _ _ _ (cong _ _ _ _ _ _ + (refl _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))) + l3)) + (trans _ _ _ _ + (row1 _ _ a i (apply _ _ (apply _ _ (read I E) a) i)) + (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) a)) l3) + ))) + l2) + +))))) (\ CT2 +; CT2 is the clause ( v2 V ~v3 ) + + +; (6) -------------------- clausification ----------------------------------------- +; --- these should introduce (holds ...) + +(satlem _ _ +(ast _ _ _ a1 (\ l1 +(clausify_false + +; input formula A1 is ( ~a1 ) +; the following is a proof of a1 ^ ( ~a1 ) => false + + (contra _ l1 A1) + +))) (\ C1 +; C1 is the clause ( ~v1 ) + + +(satlem _ _ +(asf _ _ _ a1 (\ l1 +(ast _ _ _ a2 (\ l2 +(clausify_false + +; lemma A2 is ( a1 V ~a2 ) +; the following is a proof of ~a1 ^ a2 ^ ( a1 V ~a2 ) => false + + (contra _ l2 (or_elim_1 _ _ l1 A2)) + +))))) (\ C2 +; C2 is the clause ( v1 V ~v2 ) + + +; (7) -------------------- resolution proof ------------------------------------------------------------ + +(satlem_simplify _ _ _ + +(R _ _ (R _ _ CT1 CT2 v3) (R _ _ C2 C1 v1) v2) + +(\ x x)) + +))))))))))))))))))))))))))) diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf index 6e0e6438d..edb6dc96e 100755 --- a/proofs/signatures/th_arrays.plf +++ b/proofs/signatures/th_arrays.plf @@ -12,15 +12,14 @@ ; functions (declare write (! s1 sort (! s2 sort - (! t1 (term (array s1 s2)) - (! t2 (term s1) - (! t3 (term s2) - (term (array s1 s2)))))))) + (term (arrow (array s1 s2) + (arrow s1 + (arrow s2 (array s1 s2)))))))) + (declare read (! s1 sort (! s2 sort - (! t1 (term (array s1 s2)) - (! t2 (term s1) - (term s2)))))) + (term (arrow (array s1 s2) + (arrow s1 s2)))))) ; inference rules (declare row1 (! s1 sort @@ -28,26 +27,26 @@ (! t1 (term (array s1 s2)) (! t2 (term s1) (! t3 (term s2) - (th_holds (= _ (read (write t1 t2 t3) t2) t3)))))))) + (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2) + t3)))))))) (declare row (! s1 sort (! s2 sort - (! t1 (term (array s1 s2)) (! t2 (term s1) (! t3 (term s1) + (! t1 (term (array s1 s2)) (! t4 (term s2) (! u (th_holds (not (= _ t2 t3))) - (th_holds (= _ (read (write t1 t2 t4) t3) (read t1 t3)))))))))) + (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3) + (apply _ _ (apply _ _ (read s1 s2) t1) t3))))))))))) (declare ext (! s1 sort (! s2 sort - (! f formula (! t1 (term (array s1 s2)) (! t2 (term (array s1 s2)) - (! u (th_holds (not (= _ t1 t2))) (! u1 (! k (term s1) - (! u2 (th_holds (not (= _ (read t1 k) (read t2 k)))) - (th_holds f))) - (th_holds f))))))))) + (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k))))) + (holds cln))) + (holds cln))))))) \ No newline at end of file diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf new file mode 100755 index 000000000..d18812380 --- /dev/null +++ b/proofs/signatures/th_quant.plf @@ -0,0 +1,52 @@ +(declare forall (! s sort + (! t (term s) + (! f formula + formula)))) + +(program instantiate ((f formula) (t term) (k term)) + (do (markvar t) + (let f1 (inst_f f t) + (do (markvar t) f1)))) + +(program instantiate_f ((f formula) (k term)) formula + (match f + ((and f1 f2) (and (instantiate_f f1 t) (instantiate_f f2 t))) + ((or f1 f2) (or (instantiate_f f1 t) (instantiate_f f2 t))) + ((impl f1 f2) (impl (instantiate_f f1 t) (instantiate_f f2 t))) + ((not f1) (not (instantiate_f f1 t))) + ((iff f1 f2) (iff (instantiate_f f1 t) (instantiate_f f2 t))) + ((xor f1 f2) (xor (instantiate_f f1 t) (instantiate_f f2 t))) + ((ifte f1 f2 f3) (ifte (instantiate_f f1 t) (instantiate_f f2 t) (instantiate_f f3 t))) + ((= s t1 t2) (= s (inst_t t1 t) (inst_t t2 t))) + ((forall t1 f1) (forall t1 (instantiate_f f1 t))) + (default f))) + +(program instantiate_t ((t term) (k term)) formula + (match t + ((apply s1 s2 t1 t2) (apply s1 s2 t1 (instantiate_t t2 t))) + (default (ifmarked t k t)))) + + +(declare skolem + (! s sort + (! t (term s) + (! f formula + (! p (th_holds (not (forall s t f))) + (! u (! f1 formula + (! k (term s) + (! r (^ (instantiate f t k) f1) + (! p1 (th_holds (not f1)) + (holds cln))))) + (holds cln))))))) + +(declare inst + (! s sort + (! t (term s) + (! f formula + (! f1 formula + (! p (th_holds (forall s t f)) + (! k (term s) + (! r (^ (instantiate f t k) f1) + (! u (! p1 (th_holds f1) + (holds cln)) + (holds cln)))))))))) \ No newline at end of file diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 1b34bc118..9b5e506ea 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -63,7 +63,7 @@ CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) : Assert( !d_op.isNull() ); } void CandidateGeneratorQE::resetInstantiationRound(){ - d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size(); + d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op ); } void CandidateGeneratorQE::reset( Node eqc ){ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 50a0084fc..a12fc7ca2 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -1039,7 +1039,7 @@ int QModelBuilderInstGen::getSelectionFormulaScore( Node fn ){ if( fn.getKind()==APPLY_UF ){ Node op = fn.getOperator(); //return total number of terms - return d_qe->getTermDatabase()->d_op_count[op]; + return d_qe->getTermDatabase()->d_op_nonred_count[op]; }else{ int score = 0; for( size_t i=0; igetTermDatabase()->d_op_map[f].size(); + unsigned nt = d_quantEngine->getTermDatabase()->getNumGroundTerms( f ); for( unsigned i=0; igetTermDatabase()->d_op_map[f][i]; - if( !n.getAttribute(NoMatchAttribute()) ){ - Assert( getEqualityEngine()->hasTerm( n ) ); + if( getEqualityEngine()->hasTerm( n ) && !n.getAttribute(NoMatchAttribute()) ){ Node r = getRepresentative( n ); computeArgReps( n ); d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] ); diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 20ab4e55f..914141995 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -111,7 +111,8 @@ void RelevantDomain::compute(){ TermDb * db = d_qe->getTermDatabase(); for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){ Node op = it->first; - for( unsigned i=0; isecond.size(); i++ ){ + unsigned sz = db->getNumGroundTerms( op ); + for( unsigned i=0; isecond[i]; //if it is a non-redundant term if( !n.getAttribute(NoMatchAttribute()) ){ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 08a9f5d9f..ea1231e7a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -46,6 +46,20 @@ bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ } } +TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) { + +} + +/** ground terms */ +unsigned TermDb::getNumGroundTerms( Node f ) { + std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f ); + if( it!=d_op_map.end() ){ + return it->second.size(); + }else{ + return 0; + } + //return d_op_ccount[f]; +} Node TermDb::getOperator( Node n ) { //return n.getOperator(); @@ -89,6 +103,15 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ Trace("term-db") << "register term in db " << n << std::endl; //std::cout << "register trigger term " << n << std::endl; Node op = getOperator( n ); + /* + int occ = d_op_ccount[op]; + if( occ<(int)d_op_map[op].size() ){ + d_op_map[op][occ] = n; + }else{ + d_op_map[op].push_back( n ); + } + d_op_ccount[op].set( occ + 1 ); + */ d_op_map[op].push_back( n ); added.insert( n ); @@ -120,7 +143,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ int alreadyCongruentCount = 0; //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_count[ it->first ] = 0; + d_op_nonred_count[ it->first ] = 0; if( !it->second.empty() ){ if( it->second[0].getType().isBoolean() ){ d_pred_map_trie[ 0 ][ it->first ].d_data.clear(); @@ -138,7 +161,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ congruentCount++; }else{ nonCongruentCount++; - d_op_count[ it->first ]++; + d_op_nonred_count[ it->first ]++; } }else{ congruentCount++; @@ -166,7 +189,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ congruentCount++; }else{ nonCongruentCount++; - d_op_count[ op ]++; + d_op_nonred_count[ op ]++; } }else{ alreadyCongruentCount++; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index b3db6d266..41108bc2a 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -88,6 +88,7 @@ class TermDb { friend class ::CVC4::theory::inst::Trigger; friend class ::CVC4::theory::rrinst::Trigger; friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker; + typedef context::CDHashMap NodeIntMap; private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; @@ -96,13 +97,17 @@ private: private: /** select op map */ std::map< Node, std::map< TypeNode, std::map< TypeNode, Node > > > d_par_op_map; + /** count number of ground terms per operator (user-context dependent) */ + NodeIntMap d_op_ccount; public: - TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ){} + TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); ~TermDb(){} + /** ground terms */ + unsigned getNumGroundTerms( Node f ); + /** count number of non-redundant ground terms per operator */ + std::map< Node, int > d_op_nonred_count; /** map from APPLY_UF operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; - /** count number of APPLY_UF terms per operator */ - std::map< Node, int > d_op_count; /** map from APPLY_UF functions to trie */ std::map< Node, TermArgTrie > d_func_map_trie; /** map from APPLY_UF predicates to trie */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 02423e54d..7fa61477f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -45,7 +45,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_te( te ), d_lemmas_produced_c(u){ d_eq_query = new EqualityQueryQuantifiersEngine( this ); - d_term_db = new quantifiers::TermDb( this ); + d_term_db = new quantifiers::TermDb( c, u, this ); d_tr_trie = new inst::TriggerTrie; //d_rr_tr_trie = new rrinst::TriggerTrie; //d_eem = new EfficientEMatcher( this ); diff --git a/test/regress/regress0/push-pop/bug326.smt2 b/test/regress/regress0/push-pop/bug326.smt2 index 51d60e920..8fe88e9f5 100644 --- a/test/regress/regress0/push-pop/bug326.smt2 +++ b/test/regress/regress0/push-pop/bug326.smt2 @@ -31,7 +31,7 @@ (check-sat) (pop) -; EXPECT: unknown +; EXPECT: sat (push);;sat (assert (and (not (R e1 e3)) (R e4 e1))) (check-sat) -- 2.30.2