--- /dev/null
+; 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))
+
+)))))))))))))))))))))))))))
; functions\r
(declare write (! s1 sort\r
(! s2 sort\r
- (! t1 (term (array s1 s2))\r
- (! t2 (term s1)\r
- (! t3 (term s2)\r
- (term (array s1 s2))))))))\r
+ (term (arrow (array s1 s2) \r
+ (arrow s1 \r
+ (arrow s2 (array s1 s2))))))))\r
+ \r
(declare read (! s1 sort\r
(! s2 sort\r
- (! t1 (term (array s1 s2))\r
- (! t2 (term s1)\r
- (term s2))))))\r
+ (term (arrow (array s1 s2)\r
+ (arrow s1 s2))))))\r
\r
; inference rules\r
(declare row1 (! s1 sort\r
(! t1 (term (array s1 s2))\r
(! t2 (term s1)\r
(! t3 (term s2)\r
- (th_holds (= _ (read (write t1 t2 t3) t2) t3))))))))\r
+ (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2) \r
+ t3))))))))\r
\r
\r
(declare row (! s1 sort\r
(! s2 sort\r
- (! t1 (term (array s1 s2))\r
(! t2 (term s1)\r
(! t3 (term s1)\r
+ (! t1 (term (array s1 s2))\r
(! t4 (term s2)\r
(! u (th_holds (not (= _ t2 t3)))\r
- (th_holds (= _ (read (write t1 t2 t4) t3) (read t1 t3))))))))))\r
+ (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3) \r
+ (apply _ _ (apply _ _ (read s1 s2) t1) t3)))))))))))\r
\r
(declare ext (! s1 sort\r
(! s2 sort\r
- (! f formula\r
(! t1 (term (array s1 s2))\r
(! t2 (term (array s1 s2))\r
- (! u (th_holds (not (= _ t1 t2)))\r
(! u1 (! k (term s1)\r
- (! u2 (th_holds (not (= _ (read t1 k) (read t2 k))))\r
- (th_holds f)))\r
- (th_holds f)))))))))\r
+ (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k)))))\r
+ (holds cln)))\r
+ (holds cln)))))))\r
\ No newline at end of file
--- /dev/null
+(declare forall (! s sort\r
+ (! t (term s)\r
+ (! f formula\r
+ formula))))\r
+\r
+(program instantiate ((f formula) (t term) (k term))\r
+ (do (markvar t) \r
+ (let f1 (inst_f f t)\r
+ (do (markvar t) f1))))\r
+\r
+(program instantiate_f ((f formula) (k term)) formula\r
+ (match f \r
+ ((and f1 f2) (and (instantiate_f f1 t) (instantiate_f f2 t)))\r
+ ((or f1 f2) (or (instantiate_f f1 t) (instantiate_f f2 t)))\r
+ ((impl f1 f2) (impl (instantiate_f f1 t) (instantiate_f f2 t)))\r
+ ((not f1) (not (instantiate_f f1 t)))\r
+ ((iff f1 f2) (iff (instantiate_f f1 t) (instantiate_f f2 t)))\r
+ ((xor f1 f2) (xor (instantiate_f f1 t) (instantiate_f f2 t)))\r
+ ((ifte f1 f2 f3) (ifte (instantiate_f f1 t) (instantiate_f f2 t) (instantiate_f f3 t)))\r
+ ((= s t1 t2) (= s (inst_t t1 t) (inst_t t2 t)))\r
+ ((forall t1 f1) (forall t1 (instantiate_f f1 t)))\r
+ (default f)))\r
+\r
+(program instantiate_t ((t term) (k term)) formula\r
+ (match t\r
+ ((apply s1 s2 t1 t2) (apply s1 s2 t1 (instantiate_t t2 t)))\r
+ (default (ifmarked t k t))))\r
+\r
+\r
+(declare skolem\r
+ (! s sort\r
+ (! t (term s)\r
+ (! f formula\r
+ (! p (th_holds (not (forall s t f)))\r
+ (! u (! f1 formula\r
+ (! k (term s)\r
+ (! r (^ (instantiate f t k) f1)\r
+ (! p1 (th_holds (not f1))\r
+ (holds cln)))))\r
+ (holds cln)))))))\r
+ \r
+(declare inst\r
+ (! s sort\r
+ (! t (term s)\r
+ (! f formula\r
+ (! f1 formula\r
+ (! p (th_holds (forall s t f))\r
+ (! k (term s)\r
+ (! r (^ (instantiate f t k) f1)\r
+ (! u (! p1 (th_holds f1)\r
+ (holds cln))\r
+ (holds cln))))))))))
\ No newline at end of file
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 ){
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++ ){
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
void QuantConflictFind::computeUfTerms( TNode f ) {\r
if( d_uf_terms.find( f )==d_uf_terms.end() ){\r
d_uf_terms[f].clear();\r
- unsigned nt = d_quantEngine->getTermDatabase()->d_op_map[f].size();\r
+ unsigned nt = d_quantEngine->getTermDatabase()->getNumGroundTerms( f );\r
for( unsigned i=0; i<nt; i++ ){\r
Node n = d_quantEngine->getTermDatabase()->d_op_map[f][i];\r
- if( !n.getAttribute(NoMatchAttribute()) ){\r
- Assert( getEqualityEngine()->hasTerm( n ) );\r
+ if( getEqualityEngine()->hasTerm( n ) && !n.getAttribute(NoMatchAttribute()) ){\r
Node r = getRepresentative( n );\r
computeArgReps( n );\r
d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );\r
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()) ){
}
}
+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();
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 );
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();
congruentCount++;
}else{
nonCongruentCount++;
- d_op_count[ it->first ]++;
+ d_op_nonred_count[ it->first ]++;
}
}else{
congruentCount++;
congruentCount++;
}else{
nonCongruentCount++;
- d_op_count[ op ]++;
+ d_op_nonred_count[ op ]++;
}
}else{
alreadyCongruentCount++;
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;
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 */
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 );
(check-sat)
(pop)
-; EXPECT: unknown
+; EXPECT: sat
(push);;sat
(assert (and (not (R e1 e3)) (R e4 e1)))
(check-sat)
projects / cvc5.git / commitdiff