diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-12 14:25:25 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-12 14:25:25 -0500 |
commit | 8b41e8d8128752eba75f32f751ec9c095a6b1d87 (patch) | |
tree | 68559af9be49966dedfa877b124f76d3af152b7b | |
parent | 15d36d99363b4ee20754498b566bd315150953fc (diff) |
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.
-rwxr-xr-x | proofs/signatures/example-arrays.plf | 139 | ||||
-rwxr-xr-x | proofs/signatures/th_arrays.plf | 29 | ||||
-rwxr-xr-x | proofs/signatures/th_quant.plf | 52 | ||||
-rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 29 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 11 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 | ||||
-rw-r--r-- | test/regress/regress0/push-pop/bug326.smt2 | 2 |
12 files changed, 248 insertions, 30 deletions
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; i<fn.getNumChildren(); i++ ){ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 7ee416c4e..0865f2c0b 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -125,7 +125,7 @@ option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h" when to invoke conflict find mechanism for quantifiers -option quantRewriteRules --rewrite-rules bool :default false +option quantRewriteRules --rewrite-rules bool :default true use rewrite rules module option rrOneInstPerRound --rr-one-inst-per-round bool :default false add one instance of rewrite rule per round diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 51d69ace4..c0b318f23 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2194,11 +2194,10 @@ void QuantConflictFind::computeArgReps( TNode n ) { void QuantConflictFind::computeUfTerms( TNode f ) {
if( d_uf_terms.find( f )==d_uf_terms.end() ){
d_uf_terms[f].clear();
- unsigned nt = d_quantEngine->getTermDatabase()->d_op_map[f].size();
+ unsigned nt = d_quantEngine->getTermDatabase()->getNumGroundTerms( f );
for( unsigned i=0; i<nt; i++ ){
Node n = d_quantEngine->getTermDatabase()->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; i<it->second.size(); i++ ){ + unsigned sz = db->getNumGroundTerms( op ); + for( unsigned i=0; i<sz; i++ ){ Node n = it->second[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<Node, int, NodeHashFunction> 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) |