import aiger_analysis as aa
import aiger

x, y = aiger.atom('x'), aiger.atom('y')
expr = x & y

# Call a SAT solver to check if there is a satisfying assignment.
`assert aa.is_satisfiable(expr)`

# Check if all assignments are satisfying, using a satsolver.
`assert not aa.is_valid(expr)`

# Check if two expressions are equal, using a satsolver.
`assert aa.is_equal(expr, aa.simplify(expr))`

# One can convert a boolean expression to a bdd via:
f, manager, relabels = aa.to_bdd(expr) 

# or given an aiger circuit, one can convert to a bdd by specifying the output.
# If the aiger circuit only has one output, the output does not need to be
# specificed.

f, manager, relabels = aa.to_bdd(expr.aig, output=expr.output)

# f is now a bdd expression and manager is the bdd manager. 

# Because aiger supports a larger set of names than the dd package,
# the inputs of the expression are relabeled to names given by the
# bidict relabels.

# One can convert back to an aiger boolean expression via:
expr2 = aa.from_bdd(f)

# We currently also implement counting the number of satisifying solutions using BDDs.
# This is done by first converting an expression to a bdd and the using the bdd's count
# primative.
c = aa.count(expr, percent=True)

'''
 Call the QBF solver CADET to check if this QBF is true. The second argument
 indicates the quantifier prefix: 'a' stands for universal quantifiers, 'e' for
 existential quantifiers. Each quantifier indicates a list of bound variables.
 All variables of the expression must be bound by some quantifier.
'''
assert not aa.is_true_QBF(expr, [('a', ['x']), ('e', ['y'])])

'''
 Call CADET to eliminate a given list of variables from the expression. The
 resulting expression is a formula over the remaining variables that is true
 if, and only if, there is a satisfying assignment to the indicated variables.
'''
also_x = aa.eliminate(expr, ['y'])
assert aa.is_equal(x, also_x)