equiv

example.smt2

(declare-rel inv (Int))
(declare-var x0 Int)
(declare-var x1 Int)
(declare-rel fail ())

(rule (=> (= x0 10) (inv x0)))

(rule (=> (and (inv x0) (= x1 (+ x0 x0))) (inv x1)))

(rule (=> 
	(and 
		(inv x0)
		(not (> x0 0))
	)
	fail
))

(query fail :print-certificate true)

gistfile1.txt

    // TODO: check equivalence between programs encoded in ruleManager1 and ruleManager2                                          

    SMTUtils s(efac);
    // s.isSat(ruleManager1.failDecl);                                                                                            

    // Process Program 1 (in CHC form)                                                                                            
    Expr aExpr = mk<TRUE> (efac);
    Expr a_pre_cond = mk<TRUE> (efac);
    Expr a_post_cond = mk<TRUE> (efac);
    for(auto & a : ruleManager1.chcs) {
        // We only consider Fact and Inductive, NOT Query                                                                         
        if(a.isFact) {
            // In the body of the fact, replace dstVars                                                                           
            // (primes) by the invariant variables (unprimed),                                                                    
            // that can be accessed from this data structure                                                                      

            //ruleManager1.invVars // map<Expr, ExprVector>                                                                       
            //a.dstVars //ExprVector;                                                                                             
            aExpr = boolop::land(aExpr, a.body);
        }
        if(a.isInductive) {
            // Create relational pre- and post-conditions                                                                         
            // by AND-ing equalities over srcVars of the                                                                          
            // inductive rule, and dstVars of the inductive                                                                       
            // rule, respectively.                                                                                                

            // Creating Precondition:                                                                                             
            for (auto & unprime_var : a.srcVars) {
                mk<EQ> (var1, var2); // we want var1 to come from program 1 and var 2 to come from program 2                      
                // access the source variables for first program, and source variables from program 2 and make equality for them  
                // same for dest variables                                                                                        
                // conjoin those equalities                                                                                       
                // conjoin this with the transition relation stored in a.body                                                     
                // throw this whole conjunction into the smt solver                                                               
                //                         
                                // throw this whole conjunction into the smt solver                                                               
		//                                                                                                                
                // queries and initial conditions can be a heuristic to match vars from the programs together                     
                a_pre_cond = boolop::land(a_pre_cond, unprime_var);
            }

            // Creating Postcondition:                                                                                            
            for (auto & prime_var : a.dstVars) {
                a_post_cond = boolop::land(a_post_cond, prime_var);
            }
        }
    }

    // Process Program 2 (in CHC form)                                                                                            
    Expr bExpr = mk<TRUE> (efac);
    Expr b_pre_cond = mk<TRUE> (efac);
    Expr b_post_cond = mk<TRUE> (efac);
    for(auto & b : ruleManager2.chcs) {
        // We only consider Fact and Inductive, NOT Query                                                                         
        if(b.isFact) {
            bExpr = boolop::land(bExpr, b.body);
        }
        if(b.isInductive) {
            // Create relational pre- and post-conditions                                                                         
            // by AND-ing equalities over srcVars of the                                                                          
            // inductive rule, and dstVars of the inductive                                                                       
            // rule, respectively.                                                                                                

            // Creating Precondition:                                                                                             
            for (auto & unprime_var : b.srcVars) {
                b_pre_cond = boolop::land(b_pre_cond, unprime_var);
            }

            // Creating Postcondition:                                                                                            
            for (auto & prime_var : b.dstVars) {
                b_post_cond = boolop::land(b_post_cond, prime_var);
            }
        }
    }
    // Negate the postcondition                                                                                                   
    a_post_cond = boolop::lneg(a_post_cond);
    b_post_cond = boolop::lneg(b_post_cond);
    // "Conjoin Everything"                                                                                                       
    Expr res_pls = mk<TRUE> (efac);
    res_pls = boolop::land(res_pls, a_pre_cond);
    res_pls = boolop::land(res_pls, b_pre_cond);
    res_pls = boolop::land(res_pls, a_post_cond);
    res_pls = boolop::land(res_pls, b_post_cond);
    res_pls = boolop::land(res_pls, aExpr); // maybe??                                                                            
    res_pls = boolop::land(res_pls, bExpr); // ??                                                                                 
    // and call SMTUtils::isFalse.                                                                                                
    bool res = s.isFalse(res_pls);
    outs () << res << "\n";