search

RafaelTupynamba / GuidedSampler

GuidedSampler: Coverage-guided Sampling of SMT Solutions
BSD 3-Clause "New" or "Revised" License
12 stars 2 forks source link

Could not read input formula error without cause #1

Closed JensGM closed 3 years ago

JensGM commented 3 years ago

Hey,

I tried this tool with some AST-like setup and got an error "Could not read input formula." without much more info. z3 accepts the formula.

This is the formula I used:

(declare-datatypes ((XunType 0)) (((XunType0) (XunType1) (XunType2))))
 (declare-datatypes ((AnyType 0)) (((AnyType0) (AnyType1) (AnyType2))))
 (declare-datatypes ((Identifier 0)) (((XunIdentifier (xreferent XunType)) (AnyIdentifier (areferent AnyType)))))
 (declare-datatypes ((IdentifierTuple 0)) (((IdentifierTuple (a Identifier) (b Identifier)))))
 (declare-datatypes ((Target 0)) (((PyListTarget (a Identifier) (b Identifier)) (UnpackTarget (tuple IdentifierTuple)) (NameTarget (identifier Identifier)))))
 (declare-datatypes ((NonTerminalType 0)) (((AnyType (AnyType AnyType)) (XunType (XunType XunType)))))
 (declare-datatypes ((PyList 0)) (((PyList (type NonTerminalType)))))
 (declare-datatypes ((Operator 0)) (((Add) (Sub) (Mult) (MatMult) (Div) (Mod) (Pow) (LShift) (RShift) (BitOr) (BitXor) (BitAnd) (FloorDiv))))
 (declare-datatypes ((UnaryOp 0)) (((Invert) (Not) (UAdd) (USub))))
 (declare-datatypes ((BoolOp 0)) (((And) (Or))))
 (declare-datatypes ((Expr 0)) (((BoolOpExpr (b_lhs AnyType) (b_op BoolOp) (b_rhs AnyType)) (BinOpExpr (lhs AnyType) (op Operator) (rhs AnyType)) (UnaryOpExpr (u_op UnaryOp) (operand AnyType)) (NameExpr (name_value Identifier)) (PyListExpr (list_value PyList)))))
 (declare-datatypes ((Assign 0)) (((Assign (target Target) (value Expr)))))
 (declare-datatypes ((Stmt 0)) (((ExprStmt (value Expr)) (AssignStmt (assign Assign)))))
 (declare-datatypes ((Body 0)) (((append (head Stmt) (tail Body)) (Body_root (root Stmt)))))
(check-sat)
RafaelTupynamba commented 3 years ago

Hello, The tool currently supports formulas written in the QF_AUFBV logic of SMT-LIB and its sublogics, such as QF_ABV and QF_BV. https://smtlib.cs.uiowa.edu/logics.shtml So the formulas can have only arrays, uninterpreted functions and bitvectors. You could try to encode your benchmark in QF_AUFBV, or you could extend GuidedSampler to work over other datatypes. We believe the algorithm could work well over some other datatypes, theories and logics, but we haven't implemented those extensions yet. Your formula seems to be using the theory of list, right?