summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xproofs/signatures/example-arrays.plf139
-rwxr-xr-xproofs/signatures/th_arrays.plf29
-rwxr-xr-xproofs/signatures/th_quant.plf52
-rw-r--r--src/theory/quantifiers/candidate_generator.cpp2
-rw-r--r--src/theory/quantifiers/model_builder.cpp2
-rw-r--r--src/theory/quantifiers/options2
-rwxr-xr-xsrc/theory/quantifiers/quant_conflict_find.cpp5
-rw-r--r--src/theory/quantifiers/relevant_domain.cpp3
-rw-r--r--src/theory/quantifiers/term_database.cpp29
-rw-r--r--src/theory/quantifiers/term_database.h11
-rw-r--r--src/theory/quantifiers_engine.cpp2
-rw-r--r--test/regress/regress0/push-pop/bug326.smt22
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback