Adt chc

bench/run-bench.sh

@@ -0,0 +1,49 @@
+#!/bin/bash
+echo "This is the script for running regression tests"
+echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')"
+echo " - host name $(hostname -f)"
+echo " - script path: $(readlink -f $0)"
+
+adtchc=../adtchc
+if [[ ! $# -eq 0 ]] ; then
+    #echo 'Setting path to' $1
+    adtchc=$1
+fi
+
+# run the interpolating version of OpenSMT
+adtchc=${adtchc}' -i'
+
+picky=./utils/picky.smt2
+lookahead=./utils/lookahead.smt2
+
+tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S')
+mkdir ${tmpfolder}
+
+export outmod=false
+export errmod=false
+export rtmod=false
+export err=false
+
+for file in $(find . -name '*.smt2' |sort); do
+    name=$(basename $file)
+    dir=$(dirname $file)
+
+    sh -c "ulimit -St 60; ${adtchc} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for benchmark $file";
+        err=true;
+    fi
+
+
+done
+#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}"
+
+if [[ ${err} == true ]]; then
+    echo "There were anomalies: check logs in ${tmpfolder}"
+    exit 1
+else
+    rm -rf ${tmpfolder}
+fi
+

bench_adt/run-bench.sh

@@ -0,0 +1,77 @@
+#!/bin/bash
+echo "This is the script for running regression tests"
+echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')"
+echo " - host name $(hostname -f)"
+echo " - script path: $(readlink -f $0)"
+
+opensmt=../opensmt
+if [[ ! $# -eq 0 ]] ; then
+    #echo 'Setting path to' $1
+    opensmt=$1
+fi
+
+# run the interpolating version of OpenSMT
+opensmt=${opensmt}' -i'
+
+picky=./utils/picky.smt2
+lookahead=./utils/lookahead.smt2
+
+tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S')
+mkdir ${tmpfolder}
+
+export outmod=false
+export errmod=false
+export rtmod=false
+export err=false
+
+for file in $(find . -name '*.smt2' |sort); do
+    name=$(basename $file)
+    dir=$(dirname $file)
+
+    sh -c "ulimit -St 60; ${opensmt} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null 
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for benchmark $file";
+        err=true;
+    fi
+
+    sh -c "ulimit -St 60; ${opensmt} $picky $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for picky benchmark $file";
+        err=true;
+    fi
+
+    sh -c "ulimit -St 60; ${opensmt} $lookahead $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for lookahead benchmark $file";
+        err=true;
+    fi
+
+    #diff -q ${tmpfolder}/${name}.out ${dir}/${name}.expected.out
+    #if [ $? != 0 ]; then
+    #    echo "stdout differs for benchmark $file";
+    #    outmod=true;
+    #    diff ${tmpfolder}/${name}.out ${dir}/${name}.expected.out
+    #fi
+    #diff -q ${tmpfolder}/${name}.err ${dir}/${name}.expected.err
+    #if [ $? != 0 ]; then
+    #    echo "stderr differs for benchmark $file";
+    #    errmod=true;
+    #    diff ${tmpfolder}/${name}.err ${dir}/${name}.expected.err
+    #fi
+
+done
+#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}"
+
+if [[ ${err} == true ]]; then
+    echo "There were anomalies: check logs in ${tmpfolder}"
+    exit 1
+else
+    rm -rf ${tmpfolder}
+fi
+

bench_horn_adt/ADTIND/list_len_acc.smt2

@@ -0,0 +1,10 @@
+(set-logic HORN)
+(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil))))
+(declare-fun length (Lst Int) Bool)
+(declare-fun ff () Bool)
+(assert (length nil 0))
+
+(assert (forall ((x Int) (xs Lst) (ys Lst) (l Int))
+       (=> (and (= xs (cons x ys)) (length ys l) (not (length (tail xs) l))) ff)))
+(assert (not ff))
+(check-sat)

bench_horn_adt/ADTIND/list_value_check_acc.smt2

@@ -0,0 +1,11 @@
+;There is some weird error rn
+(set-logic HORN)
+(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil))))
+(declare-fun length (Lst Int) Bool)
+(declare-fun ff () Bool)
+
+;(assert (length nil 0))
+(assert (forall ((x1 Int) (x2 Int) (xs Lst) (ys Lst) (zs Lst) (l Int))
+       (=> (and (= xs (cons x1 ys)) (= ys (cons x2 zs)) (not (= (head (tail xs)) x2))) ff)))
+(assert (not ff))
+(check-sat)

bench_horn_adt/run-bench.sh

@@ -0,0 +1,49 @@
+#!/bin/bash
+echo "This is the script for running regression tests"
+echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')"
+echo " - host name $(hostname -f)"
+echo " - script path: $(readlink -f $0)"
+
+adtchc=../adtchc
+if [[ ! $# -eq 0 ]] ; then
+    #echo 'Setting path to' $1
+    adtchc=$1
+fi
+
+# run the interpolating version of OpenSMT
+adtchc=${adtchc}' -i'
+
+picky=./utils/picky.smt2
+lookahead=./utils/lookahead.smt2
+
+tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S')
+mkdir ${tmpfolder}
+
+export outmod=false
+export errmod=false
+export rtmod=false
+export err=false
+
+for file in $(find . -name '*.smt2' |sort); do
+    name=$(basename $file)
+    dir=$(dirname $file)
+
+    sh -c "ulimit -St 60; ${adtchc} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for benchmark $file";
+        err=true;
+    fi
+
+
+done
+#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}"
+
+if [[ ${err} == true ]]; then
+    echo "There were anomalies: check logs in ${tmpfolder}"
+    exit 1
+else
+    rm -rf ${tmpfolder}
+fi
+

bench_sim/run-bench.sh

@@ -0,0 +1,49 @@
+#!/bin/bash
+echo "This is the script for running regression tests"
+echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')"
+echo " - host name $(hostname -f)"
+echo " - script path: $(readlink -f $0)"
+
+adtchc=../adtchc
+if [[ ! $# -eq 0 ]] ; then
+    #echo 'Setting path to' $1
+    adtchc=$1
+fi
+
+# run the interpolating version of OpenSMT
+adtchc=${adtchc}' -i'
+
+picky=./utils/picky.smt2
+lookahead=./utils/lookahead.smt2
+
+tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S')
+mkdir ${tmpfolder}
+
+export outmod=false
+export errmod=false
+export rtmod=false
+export err=false
+
+for file in $(find . -name '*.smt2' |sort); do
+    name=$(basename $file)
+    dir=$(dirname $file)
+
+    sh -c "ulimit -St 60; ${adtchc} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+
+    if [ -s "$tmpfolder/$name.err" ]; then
+        echo "stderr not empty for benchmark $file";
+        err=true;
+    fi
+
+
+done
+#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}"
+
+if [[ ${err} == true ]]; then
+    echo "There were anomalies: check logs in ${tmpfolder}"
+    exit 1
+else
+    rm -rf ${tmpfolder}
+fi
+

include/adt/CHCSolver.hpp

@@ -18,6 +18,7 @@ namespace ufo
     // Keep the current return values
     std::map<Expr,int> values_inds;
     ExprVector &constructors;
+    ExprVector &accessors;
     ExprVector &assumptions;
 
     ExprSet &decls;
@@ -35,8 +36,8 @@ namespace ufo
     map<Expr, Expr> interpretations;
 
   public:
-    CHCSolver(ExprVector& _constructors, ExprSet& _adts, ExprFactory &_efac, ExprSet &_decls, ExprVector &_assms, vector<HornRuleExt> &_chcs, bool _nonadtPriority = false, bool _ignoreBase = false) :
-      constructors(_constructors), adts(_adts), efac(_efac), decls(_decls), assumptions(_assms), chcs(_chcs), givePriority(_nonadtPriority), ignoreBaseVar(_ignoreBase) {}
+    CHCSolver(ExprVector& _constructors, ExprVector& _accessors, ExprSet& _adts, ExprFactory &_efac, ExprSet &_decls, ExprVector &_assms, vector<HornRuleExt> &_chcs, bool _nonadtPriority = false, bool _ignoreBase = false) :
+      constructors(_constructors), accessors(_accessors), adts(_adts), efac(_efac), decls(_decls), assumptions(_assms), chcs(_chcs), givePriority(_nonadtPriority), ignoreBaseVar(_ignoreBase) {}
 
     Expr createNewApp(HornRuleExt chc, int i, int ind) {
       ExprVector types;
@@ -92,6 +93,17 @@ namespace ufo
           }
         }
       }
+      // TODO: HERE I NEED TO CHECK IF WHAT I HAVE ON THE RIGHT IS AN ACCESSOR
+      if ((elem->right()->arity() == 2) && isAccessor(bind::fname(elem->right()))) {
+        matching[elem->right()] = elem->left();
+        return true;
+      }
+
+      else if ((elem->left()->arity() == 2) && isAccessor(bind::fname(elem->left()))) {
+        matching[elem->left()] = elem->right();
+        return true;
+      }
+      // TODO: HERE I CAN CHECK IF ACCESSOR, AND THEN DO THE REVERSE MATCHING, SO HEAD(SMTH) -> X, NOT X -> HEAD(SMTH)
       if ((elem->left()->arity() == 1) && !(isConstructor(bind::fname(elem->left())))) {
           matching[elem->left()] = elem->right();
           return true;
@@ -127,6 +139,11 @@ namespace ufo
       return std::find(constructors.begin(), constructors.end(), elem) != constructors.end();
     }
 
+
+    bool isAccessor(Expr elem) {
+      return std::find(accessors.begin(), accessors.end(), fname(elem)) != accessors.end();
+    }
+
     Expr createDestination(HornRuleExt chc) {
       int ind = values_inds[chc.dstRelation->left()];
       ExprVector types;
@@ -465,10 +482,8 @@ namespace ufo
           // add functions for filter variables here
           if (ignoreBaseVar) excludeBaseVar(cur, idxs);
           if (givePriority) givePriorityNonAdt(cur, idxs);
-           // outs() << *chc.dstRelation->left() << " " << idxs.size() << "\n";
           for (int i = idxs.size() - 1; i >= 0; --i) {
             buf[chc.dstRelation->left()] = idxs[i];
-            // outs() << *chc.dstRelation->left() << " " << idxs[i] << "\n";
             if (findInterpretations(idx + 1, buf))
               return true;
           }
@@ -481,7 +496,6 @@ namespace ufo
     bool solve() {
       // Order current uninterpreted predicate symbols
       for (auto & decl: decls) {
-        // outs() << *decl << "\n";
         ExprSet cur_decls;
         if (!orderDecls(decl, cur_decls))
           return false;
@@ -581,6 +595,7 @@ namespace ufo
     // ruleManager.print();
 
     ExprVector constructors;
+    ExprVector accessors;
 
     ExprSet& decls = ruleManager.decls;
 
@@ -589,7 +604,12 @@ namespace ufo
       adts.insert(a->last());
     }
 
-    CHCSolver sol (constructors, adts, efac, decls, ruleManager.extras, ruleManager.chcs,
+    for (auto & a : z3.getAdtAccessors()) {
+      accessors.push_back(regularizeQF(a));
+      adts.insert(a->last());
+    }
+
+    CHCSolver sol (constructors, accessors, adts, efac, decls, ruleManager.extras, ruleManager.chcs,
       givePriorityNonAdt, ignoreBaseVar);
     bool res = containsOp<ARRAY_TY>(conjoin(decls, efac)) ? sol.solveArr() : sol.solve();
     outs () << (res ? "sat\n" : "unknown\n");

include/deep/HornNonlin.hpp

@@ -108,8 +108,9 @@ namespace ufo
       for (auto c = lin.begin(); c != lin.end(); )
       {
         Expr cnj = *c;
-        if (isOpX<FAPP>(cnj) && isOpX<FDECL>(cnj->left()))
+        if (isOpX<FAPP>(cnj))
         {
+          assert(isOpX<FDECL>(cnj->left()));
           Expr rel = cnj->arg(0);
           addDecl(rel);
           srcRelations.push_back(rel);